author  hoelzl 
Mon, 23 Aug 2010 19:35:57 +0200  
changeset 38656  d5d342611edb 
parent 37591  d3daea901123 
child 39096  111756225292 
permissions  rwrr 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

1 
header {*Caratheodory Extension Theorem*} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

2 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

3 
theory Caratheodory 
38656  4 
imports Sigma_Algebra Positive_Infinite_Real 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

5 
begin 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

6 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

7 
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

8 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

9 
subsection {* Measure Spaces *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

10 

38656  11 
definition "positive f \<longleftrightarrow> f {} = (0::pinfreal)"  "Positive is enforced by the type" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

12 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

13 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

14 
additive where 
38656  15 
"additive M f \<longleftrightarrow> 
16 
(\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

17 
\<longrightarrow> f (x \<union> y) = f x + f y)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

18 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

19 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

20 
countably_additive where 
38656  21 
"countably_additive M f \<longleftrightarrow> 
22 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

23 
disjoint_family A \<longrightarrow> 
38656  24 
(\<Union>i. A i) \<in> sets M \<longrightarrow> 
25 
(\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i))" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

26 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

27 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

28 
increasing where 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

29 
"increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

30 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

31 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

32 
subadditive where 
38656  33 
"subadditive M f \<longleftrightarrow> 
34 
(\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

35 
\<longrightarrow> f (x \<union> y) \<le> f x + f y)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

36 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

37 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

38 
countably_subadditive where 
38656  39 
"countably_subadditive M f \<longleftrightarrow> 
40 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

41 
disjoint_family A \<longrightarrow> 
38656  42 
(\<Union>i. A i) \<in> sets M \<longrightarrow> 
43 
f (\<Union>i. A i) \<le> psuminf (\<lambda>n. f (A n)))" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

44 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

45 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

46 
lambda_system where 
38656  47 
"lambda_system M f = 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

48 
{l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M  l) \<inter> x) = f x)}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

49 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

50 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

51 
outer_measure_space where 
38656  52 
"outer_measure_space M f \<longleftrightarrow> 
53 
positive f \<and> increasing M f \<and> countably_subadditive M f" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

54 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

55 
definition 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

56 
measure_set where 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

57 
"measure_set M f X = 
38656  58 
{r . \<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>\<^isub>\<infinity> i. f (A i)) = r}" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

59 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

60 
locale measure_space = sigma_algebra + 
38656  61 
fixes \<mu> :: "'a set \<Rightarrow> pinfreal" 
62 
assumes empty_measure [simp]: "\<mu> {} = 0" 

63 
and ca: "countably_additive M \<mu>" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

64 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

65 
lemma increasingD: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

66 
"increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

67 
by (auto simp add: increasing_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

68 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

69 
lemma subadditiveD: 
38656  70 
"subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

71 
\<Longrightarrow> f (x \<union> y) \<le> f x + f y" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

72 
by (auto simp add: subadditive_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

73 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

74 
lemma additiveD: 
38656  75 
"additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

76 
\<Longrightarrow> f (x \<union> y) = f x + f y" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

77 
by (auto simp add: additive_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

78 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

79 
lemma countably_additiveD: 
35582  80 
"countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A 
38656  81 
\<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i)" 
35582  82 
by (simp add: countably_additive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

83 

38656  84 
section "Extend binary sets" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

85 

35582  86 
lemma LIMSEQ_binaryset: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

87 
assumes f: "f {} = 0" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

88 
shows "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) > f A + f B" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

89 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

90 
have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)" 
35582  91 
proof 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

92 
fix n 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

93 
show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B" 
35582  94 
by (induct n) (auto simp add: binaryset_def f) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

95 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

96 
moreover 
35582  97 
have "... > f A + f B" by (rule LIMSEQ_const) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

98 
ultimately 
35582  99 
have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) > f A + f B" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

100 
by metis 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

101 
hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) > f A + f B" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

102 
by simp 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

103 
thus ?thesis by (rule LIMSEQ_offset [where k=2]) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

104 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

105 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

106 
lemma binaryset_sums: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

107 
assumes f: "f {} = 0" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

108 
shows "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)" 
38656  109 
by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

110 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

111 
lemma suminf_binaryset_eq: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

112 
"f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

113 
by (metis binaryset_sums sums_unique) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

114 

38656  115 
lemma binaryset_psuminf: 
116 
assumes "f {} = 0" 

117 
shows "(\<Sum>\<^isub>\<infinity> n. f (binaryset A B n)) = f A + f B" (is "?suminf = ?sum") 

118 
proof  

119 
have *: "{..<2} = {0, 1::nat}" by auto 

120 
have "\<forall>n\<ge>2. f (binaryset A B n) = 0" 

121 
unfolding binaryset_def 

122 
using assms by auto 

123 
hence "?suminf = (\<Sum>N<2. f (binaryset A B N))" 

124 
by (rule psuminf_finite) 

125 
also have "... = ?sum" unfolding * binaryset_def 

126 
by simp 

127 
finally show ?thesis . 

128 
qed 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

129 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

130 
subsection {* Lambda Systems *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

131 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

132 
lemma (in algebra) lambda_system_eq: 
38656  133 
"lambda_system M f = 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

134 
{l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x  l) = f x)}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

135 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

136 
have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M  l) \<inter> x = x  l" 
37032  137 
by (metis Int_Diff Int_absorb1 Int_commute sets_into_space) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

138 
show ?thesis 
37032  139 
by (auto simp add: lambda_system_def) (metis Int_commute)+ 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

140 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

141 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

142 
lemma (in algebra) lambda_system_empty: 
38656  143 
"positive f \<Longrightarrow> {} \<in> lambda_system M f" 
144 
by (auto simp add: positive_def lambda_system_eq) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

145 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

146 
lemma lambda_system_sets: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

147 
"x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

148 
by (simp add: lambda_system_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

149 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

150 
lemma (in algebra) lambda_system_Compl: 
38656  151 
fixes f:: "'a set \<Rightarrow> pinfreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

152 
assumes x: "x \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

153 
shows "space M  x \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

154 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

155 
have "x \<subseteq> space M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

156 
by (metis sets_into_space lambda_system_sets x) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

157 
hence "space M  (space M  x) = x" 
38656  158 
by (metis double_diff equalityE) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

159 
with x show ?thesis 
38656  160 
by (force simp add: lambda_system_def ac_simps) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

161 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

162 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

163 
lemma (in algebra) lambda_system_Int: 
38656  164 
fixes f:: "'a set \<Rightarrow> pinfreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

165 
assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

166 
shows "x \<inter> y \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

167 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

168 
from xl yl show ?thesis 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

169 
proof (auto simp add: positive_def lambda_system_eq Int) 
33536  170 
fix u 
171 
assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

172 
and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z  x) = f z" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

173 
and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z  y) = f z" 
33536  174 
have "u  x \<inter> y \<in> sets M" 
175 
by (metis Diff Diff_Int Un u x y) 

176 
moreover 

177 
have "(u  (x \<inter> y)) \<inter> y = u \<inter> y  x" by blast 

178 
moreover 

179 
have "u  x \<inter> y  y = u  y" by blast 

180 
ultimately 

181 
have ey: "f (u  x \<inter> y) = f (u \<inter> y  x) + f (u  y)" using fy 

182 
by force 

38656  183 
have "f (u \<inter> (x \<inter> y)) + f (u  x \<inter> y) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

184 
= (f (u \<inter> (x \<inter> y)) + f (u \<inter> y  x)) + f (u  y)" 
38656  185 
by (simp add: ey ac_simps) 
33536  186 
also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y  x)) + f (u  y)" 
38656  187 
by (simp add: Int_ac) 
33536  188 
also have "... = f (u \<inter> y) + f (u  y)" 
189 
using fx [THEN bspec, of "u \<inter> y"] Int y u 

190 
by force 

191 
also have "... = f u" 

38656  192 
by (metis fy u) 
33536  193 
finally show "f (u \<inter> (x \<inter> y)) + f (u  x \<inter> y) = f u" . 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

194 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

195 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

196 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

197 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

198 
lemma (in algebra) lambda_system_Un: 
38656  199 
fixes f:: "'a set \<Rightarrow> pinfreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

200 
assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

201 
shows "x \<union> y \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

202 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

203 
have "(space M  x) \<inter> (space M  y) \<in> sets M" 
38656  204 
by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

205 
moreover 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

206 
have "x \<union> y = space M  ((space M  x) \<inter> (space M  y))" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

207 
by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

208 
ultimately show ?thesis 
38656  209 
by (metis lambda_system_Compl lambda_system_Int xl yl) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

210 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

211 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

212 
lemma (in algebra) lambda_system_algebra: 
38656  213 
"positive f \<Longrightarrow> algebra (M (sets := lambda_system M f))" 
214 
apply (auto simp add: algebra_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

215 
apply (metis lambda_system_sets set_mp sets_into_space) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

216 
apply (metis lambda_system_empty) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

217 
apply (metis lambda_system_Compl) 
38656  218 
apply (metis lambda_system_Un) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

219 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

220 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

221 
lemma (in algebra) lambda_system_strong_additive: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

222 
assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

223 
and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

224 
shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

225 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

226 
have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

227 
moreover 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

228 
have "z \<inter> y = (z \<inter> (x \<union> y))  x" using disj by blast 
38656  229 
moreover 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

230 
have "(z \<inter> (x \<union> y)) \<in> sets M" 
38656  231 
by (metis Int Un lambda_system_sets xl yl z) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

232 
ultimately show ?thesis using xl yl 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

233 
by (simp add: lambda_system_eq) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

234 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

235 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

236 
lemma (in algebra) lambda_system_additive: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

237 
"additive (M (sets := lambda_system M f)) f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

238 
proof (auto simp add: additive_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

239 
fix x and y 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

240 
assume disj: "x \<inter> y = {}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

241 
and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

242 
hence "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+ 
38656  243 
thus "f (x \<union> y) = f x + f y" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

244 
using lambda_system_strong_additive [OF top disj xl yl] 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

245 
by (simp add: Un) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

246 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

247 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

248 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

249 
lemma (in algebra) countably_subadditive_subadditive: 
38656  250 
assumes f: "positive f" and cs: "countably_subadditive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

251 
shows "subadditive M f" 
35582  252 
proof (auto simp add: subadditive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

253 
fix x y 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

254 
assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

255 
hence "disjoint_family (binaryset x y)" 
35582  256 
by (auto simp add: disjoint_family_on_def binaryset_def) 
257 
hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 

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

38656  259 
f (\<Union>i. binaryset x y i) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" 
35582  260 
using cs by (simp add: countably_subadditive_def) 
261 
hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 

38656  262 
f (x \<union> y) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

263 
by (simp add: range_binaryset_eq UN_binaryset_eq) 
38656  264 
thus "f (x \<union> y) \<le> f x + f y" using f x y 
265 
by (auto simp add: Un o_def binaryset_psuminf positive_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

266 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

267 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

268 
lemma (in algebra) additive_sum: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

269 
fixes A:: "nat \<Rightarrow> 'a set" 
38656  270 
assumes f: "positive f" and ad: "additive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

271 
and A: "range A \<subseteq> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

272 
and disj: "disjoint_family A" 
38656  273 
shows "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

274 
proof (induct n) 
38656  275 
case 0 show ?case using f by (simp add: positive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

276 
next 
38656  277 
case (Suc n) 
278 
have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj 

35582  279 
by (auto simp add: disjoint_family_on_def neq_iff) blast 
38656  280 
moreover 
281 
have "A n \<in> sets M" using A by blast 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

282 
moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

283 
by (metis A UNION_in_sets atLeast0LessThan) 
38656  284 
moreover 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

285 
ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)" 
38656  286 
using ad UNION_in_sets A by (auto simp add: additive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

287 
with Suc.hyps show ?case using ad 
38656  288 
by (auto simp add: atLeastLessThanSuc additive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

289 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

290 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

291 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

292 
lemma countably_subadditiveD: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

293 
"countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> 
38656  294 
(\<Union>i. A i) \<in> sets M \<Longrightarrow> f (\<Union>i. A i) \<le> psuminf (f o A)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

295 
by (auto simp add: countably_subadditive_def o_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

296 

38656  297 
lemma (in algebra) increasing_additive_bound: 
298 
fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal" 

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

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

300 
and inc: "increasing M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

301 
and A: "range A \<subseteq> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

302 
and disj: "disjoint_family A" 
38656  303 
shows "psuminf (f \<circ> A) \<le> f (space M)" 
304 
proof (safe intro!: psuminf_bound) 

305 
fix N 

306 
have "setsum (f \<circ> A) {0..<N} = f (\<Union>i\<in>{0..<N}. A i)" 

307 
by (rule additive_sum [OF f ad A disj]) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

308 
also have "... \<le> f (space M)" using space_closed A 
38656  309 
by (blast intro: increasingD [OF inc] UNION_in_sets top) 
310 
finally show "setsum (f \<circ> A) {..<N} \<le> f (space M)" by (simp add: atLeast0LessThan) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

311 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

312 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

313 
lemma lambda_system_increasing: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

314 
"increasing M f \<Longrightarrow> increasing (M (sets := lambda_system M f)) f" 
38656  315 
by (simp add: increasing_def lambda_system_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

316 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

317 
lemma (in algebra) lambda_system_strong_sum: 
38656  318 
fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal" 
319 
assumes f: "positive f" and a: "a \<in> sets M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

320 
and A: "range A \<subseteq> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

321 
and disj: "disjoint_family A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

322 
shows "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

323 
proof (induct n) 
38656  324 
case 0 show ?case using f by (simp add: positive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

325 
next 
38656  326 
case (Suc n) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

327 
have 2: "A n \<inter> UNION {0..<n} A = {}" using disj 
38656  328 
by (force simp add: disjoint_family_on_def neq_iff) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

329 
have 3: "A n \<in> lambda_system M f" using A 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

330 
by blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

331 
have 4: "UNION {0..<n} A \<in> lambda_system M f" 
38656  332 
using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f] 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

333 
by simp 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

334 
from Suc.hyps show ?case 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

335 
by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4]) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

336 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

337 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

338 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

339 
lemma (in sigma_algebra) lambda_system_caratheodory: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

340 
assumes oms: "outer_measure_space M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

341 
and A: "range A \<subseteq> lambda_system M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

342 
and disj: "disjoint_family A" 
38656  343 
shows "(\<Union>i. A i) \<in> lambda_system M f \<and> psuminf (f \<circ> A) = f (\<Union>i. A i)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

344 
proof  
38656  345 
have pos: "positive f" and inc: "increasing M f" 
346 
and csa: "countably_subadditive M f" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

347 
by (metis oms outer_measure_space_def)+ 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

348 
have sa: "subadditive M f" 
38656  349 
by (metis countably_subadditive_subadditive csa pos) 
350 
have A': "range A \<subseteq> sets (M(sets := lambda_system M f))" using A 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

351 
by simp 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

352 
have alg_ls: "algebra (M(sets := lambda_system M f))" 
38656  353 
by (rule lambda_system_algebra) (rule pos) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

354 
have A'': "range A \<subseteq> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

355 
by (metis A image_subset_iff lambda_system_sets) 
38656  356 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

357 
have U_in: "(\<Union>i. A i) \<in> sets M" 
37032  358 
by (metis A'' countable_UN) 
38656  359 
have U_eq: "f (\<Union>i. A i) = psuminf (f o A)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

360 
proof (rule antisym) 
38656  361 
show "f (\<Union>i. A i) \<le> psuminf (f \<circ> A)" 
362 
by (rule countably_subadditiveD [OF csa A'' disj U_in]) 

363 
show "psuminf (f \<circ> A) \<le> f (\<Union>i. A i)" 

364 
by (rule psuminf_bound, unfold atLeast0LessThan[symmetric]) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

365 
(metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right 
38656  366 
lambda_system_additive subset_Un_eq increasingD [OF inc] 
367 
A' A'' UNION_in_sets U_in) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

368 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

369 
{ 
38656  370 
fix a 
371 
assume a [iff]: "a \<in> sets M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

372 
have "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) = f a" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

373 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

374 
show ?thesis 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

375 
proof (rule antisym) 
33536  376 
have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A'' 
377 
by blast 

38656  378 
moreover 
33536  379 
have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj 
38656  380 
by (auto simp add: disjoint_family_on_def) 
381 
moreover 

33536  382 
have "a \<inter> (\<Union>i. A i) \<in> sets M" 
383 
by (metis Int U_in a) 

38656  384 
ultimately 
385 
have "f (a \<inter> (\<Union>i. A i)) \<le> psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" 

386 
using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] 

387 
by (simp add: o_def) 

388 
hence "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) \<le> 

389 
psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a  (\<Union>i. A i))" 

390 
by (rule add_right_mono) 

391 
moreover 

392 
have "psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a  (\<Union>i. A i)) \<le> f a" 

393 
proof (safe intro!: psuminf_bound_add) 

33536  394 
fix n 
395 
have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" 

38656  396 
by (metis A'' UNION_in_sets) 
33536  397 
have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' 
37032  398 
by (blast intro: increasingD [OF inc] A'' UNION_in_sets) 
33536  399 
have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f" 
38656  400 
using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]] 
401 
by (simp add: A) 

402 
hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a  (\<Union>i\<in>{0..<n}. A i))" 

37032  403 
by (simp add: lambda_system_eq UNION_in) 
33536  404 
have "f (a  (\<Union>i. A i)) \<le> f (a  (\<Union>i\<in>{0..<n}. A i))" 
38656  405 
by (blast intro: increasingD [OF inc] UNION_eq_Union_image 
37032  406 
UNION_in U_in) 
38656  407 
thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {..<n} + f (a  (\<Union>i. A i)) \<le> f a" 
408 
by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) 

33536  409 
qed 
38656  410 
ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
411 
by (rule order_trans) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

412 
next 
38656  413 
have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a  (\<Union>i. A i)))" 
37032  414 
by (blast intro: increasingD [OF inc] U_in) 
33536  415 
also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i))" 
37032  416 
by (blast intro: subadditiveD [OF sa] U_in) 
33536  417 
finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i))" . 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

418 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

419 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

420 
} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

421 
thus ?thesis 
38656  422 
by (simp add: lambda_system_eq sums_iff U_eq U_in) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

423 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

424 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

425 
lemma (in sigma_algebra) caratheodory_lemma: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

426 
assumes oms: "outer_measure_space M f" 
38656  427 
shows "measure_space (space = space M, sets = lambda_system M f) f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

428 
proof  
38656  429 
have pos: "positive f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

430 
by (metis oms outer_measure_space_def) 
38656  431 
have alg: "algebra (space = space M, sets = lambda_system M f)" 
432 
using lambda_system_algebra [of f, OF pos] 

433 
by (simp add: algebra_def) 

434 
then moreover 

435 
have "sigma_algebra (space = space M, sets = lambda_system M f)" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

436 
using lambda_system_caratheodory [OF oms] 
38656  437 
by (simp add: sigma_algebra_disjoint_iff) 
438 
moreover 

439 
have "measure_space_axioms (space = space M, sets = lambda_system M f) f" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

440 
using pos lambda_system_caratheodory [OF oms] 
38656  441 
by (simp add: measure_space_axioms_def positive_def lambda_system_sets 
442 
countably_additive_def o_def) 

443 
ultimately 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

444 
show ?thesis 
38656  445 
by intro_locales (auto simp add: sigma_algebra_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

446 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

447 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

448 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

449 
lemma (in algebra) inf_measure_nonempty: 
38656  450 
assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

451 
shows "f b \<in> measure_set M f a" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

452 
proof  
38656  453 
have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}" 
454 
by (rule psuminf_finite) (simp add: f[unfolded positive_def]) 

455 
also have "... = f b" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

456 
by simp 
38656  457 
finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" . 
458 
thus ?thesis using a b 

459 
by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] 

460 
simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) 

461 
qed 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

462 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

463 
lemma (in algebra) additive_increasing: 
38656  464 
assumes posf: "positive f" and addf: "additive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

465 
shows "increasing M f" 
38656  466 
proof (auto simp add: increasing_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

467 
fix x y 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

468 
assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y" 
38656  469 
have "f x \<le> f x + f (yx)" .. 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

470 
also have "... = f (x \<union> (yx))" using addf 
37032  471 
by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2)) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

472 
also have "... = f y" 
37032  473 
by (metis Un_Diff_cancel Un_absorb1 xy(3)) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

474 
finally show "f x \<le> f y" . 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

475 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

476 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

477 
lemma (in algebra) countably_additive_additive: 
38656  478 
assumes posf: "positive f" and ca: "countably_additive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

479 
shows "additive M f" 
38656  480 
proof (auto simp add: additive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

481 
fix x y 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

482 
assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

483 
hence "disjoint_family (binaryset x y)" 
38656  484 
by (auto simp add: disjoint_family_on_def binaryset_def) 
485 
hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> 

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

487 
f (\<Union>i. binaryset x y i) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

488 
using ca 
38656  489 
by (simp add: countably_additive_def) 
490 
hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 

491 
f (x \<union> y) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

492 
by (simp add: range_binaryset_eq UN_binaryset_eq) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

493 
thus "f (x \<union> y) = f x + f y" using posf x y 
38656  494 
by (auto simp add: Un binaryset_psuminf positive_def) 
495 
qed 

496 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

497 
lemma (in algebra) inf_measure_agrees: 
38656  498 
assumes posf: "positive f" and ca: "countably_additive M f" 
499 
and s: "s \<in> sets M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

500 
shows "Inf (measure_set M f s) = f s" 
38656  501 
unfolding Inf_pinfreal_def 
502 
proof (safe intro!: Greatest_equality) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

503 
fix z 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

504 
assume z: "z \<in> measure_set M f s" 
38656  505 
from this obtain A where 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

506 
A: "range A \<subseteq> sets M" and disj: "disjoint_family A" 
38656  507 
and "s \<subseteq> (\<Union>x. A x)" and si: "psuminf (f \<circ> A) = z" 
508 
by (auto simp add: measure_set_def comp_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

509 
hence seq: "s = (\<Union>i. A i \<inter> s)" by blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

510 
have inc: "increasing M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

511 
by (metis additive_increasing ca countably_additive_additive posf) 
38656  512 
have sums: "psuminf (\<lambda>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)" 
513 
proof (rule countably_additiveD [OF ca]) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

514 
show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s 
33536  515 
by blast 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

516 
show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj 
35582  517 
by (auto simp add: disjoint_family_on_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

518 
show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s 
33536  519 
by (metis UN_extend_simps(4) s seq) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

520 
qed 
38656  521 
hence "f s = psuminf (\<lambda>i. f (A i \<inter> s))" 
37032  522 
using seq [symmetric] by (simp add: sums_iff) 
38656  523 
also have "... \<le> psuminf (f \<circ> A)" 
524 
proof (rule psuminf_le) 

525 
fix n show "f (A n \<inter> s) \<le> (f \<circ> A) n" using A s 

526 
by (force intro: increasingD [OF inc]) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

527 
qed 
38656  528 
also have "... = z" by (rule si) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

529 
finally show "f s \<le> z" . 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

530 
next 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

531 
fix y 
38656  532 
assume y: "\<forall>u \<in> measure_set M f s. y \<le> u" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

533 
thus "y \<le> f s" 
38656  534 
by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

535 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

536 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

537 
lemma (in algebra) inf_measure_empty: 
38656  538 
assumes posf: "positive f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

539 
shows "Inf (measure_set M f {}) = 0" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

540 
proof (rule antisym) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

541 
show "Inf (measure_set M f {}) \<le> 0" 
38656  542 
by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def]) 
543 
qed simp 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

544 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

545 
lemma (in algebra) inf_measure_positive: 
38656  546 
"positive f \<Longrightarrow> 
547 
positive (\<lambda>x. Inf (measure_set M f x))" 

548 
by (simp add: positive_def inf_measure_empty) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

549 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

550 
lemma (in algebra) inf_measure_increasing: 
38656  551 
assumes posf: "positive f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

552 
shows "increasing ( space = space M, sets = Pow (space M) ) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

553 
(\<lambda>x. Inf (measure_set M f x))" 
38656  554 
apply (auto simp add: increasing_def) 
555 
apply (rule complete_lattice_class.Inf_greatest) 

556 
apply (rule complete_lattice_class.Inf_lower) 

37032  557 
apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

558 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

559 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

560 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

561 
lemma (in algebra) inf_measure_le: 
38656  562 
assumes posf: "positive f" and inc: "increasing M f" 
563 
and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> psuminf (f \<circ> A) = r}" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

564 
shows "Inf (measure_set M f s) \<le> x" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

565 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

566 
from x 
38656  567 
obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" 
568 
and xeq: "psuminf (f \<circ> A) = x" 

569 
by auto 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

570 
have dA: "range (disjointed A) \<subseteq> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

571 
by (metis A range_disjointed_sets) 
38656  572 
have "\<forall>n.(f o disjointed A) n \<le> (f \<circ> A) n" unfolding comp_def 
573 
by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def) 

574 
hence sda: "psuminf (f o disjointed A) \<le> psuminf (f \<circ> A)" 

575 
by (blast intro: psuminf_le) 

576 
hence ley: "psuminf (f o disjointed A) \<le> x" 

577 
by (metis xeq) 

578 
hence y: "psuminf (f o disjointed A) \<in> measure_set M f s" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

579 
apply (auto simp add: measure_set_def) 
38656  580 
apply (rule_tac x="disjointed A" in exI) 
581 
apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

582 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

583 
show ?thesis 
38656  584 
by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

585 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

586 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

587 
lemma (in algebra) inf_measure_close: 
38656  588 
assumes posf: "positive f" and e: "0 < e" and ss: "s \<subseteq> (space M)" 
589 
shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and> 

590 
psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e" 

591 
proof (cases "Inf (measure_set M f s) = \<omega>") 

592 
case False 

593 
obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e" 

594 
using Inf_close[OF False e] by auto 

595 
thus ?thesis 

596 
by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) 

597 
next 

598 
case True 

599 
have "measure_set M f s \<noteq> {}" 

600 
by (metis emptyE ss inf_measure_nonempty [of f, OF posf top]) 

601 
then obtain l where "l \<in> measure_set M f s" by auto 

602 
moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp 

603 
ultimately show ?thesis 

604 
by (auto intro!: exI[of _ l] simp: measure_set_def comp_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

605 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

606 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

607 
lemma (in algebra) inf_measure_countably_subadditive: 
38656  608 
assumes posf: "positive f" and inc: "increasing M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

609 
shows "countably_subadditive ( space = space M, sets = Pow (space M) ) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

610 
(\<lambda>x. Inf (measure_set M f x))" 
38656  611 
unfolding countably_subadditive_def o_def 
612 
proof (safe, simp, rule pinfreal_le_epsilon) 

613 
fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal 

614 

615 
let "?outer n" = "Inf (measure_set M f (A n))" 

616 
assume A: "range A \<subseteq> Pow (space M)" 

617 
and disj: "disjoint_family A" 

618 
and sb: "(\<Union>i. A i) \<subseteq> space M" 

619 
and e: "0 < e" 

620 
hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and> 

621 
A n \<subseteq> (\<Union>i. BB n i) \<and> 

622 
psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)" 

623 
apply (safe intro!: choice inf_measure_close [of f, OF posf _]) 

624 
using e sb by (cases e, auto simp add: not_le mult_pos_pos) 

625 
then obtain BB 

626 
where BB: "\<And>n. (range (BB n) \<subseteq> sets M)" 

627 
and disjBB: "\<And>n. disjoint_family (BB n)" 

628 
and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)" 

629 
and BBle: "\<And>n. psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)" 

630 
by auto blast 

631 
have sll: "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> psuminf ?outer + e" 

632 
proof  

633 
have "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> (\<Sum>\<^isub>\<infinity> n. ?outer n + e*(1/2) ^ Suc n)" 

634 
by (rule psuminf_le[OF BBle]) 

635 
also have "... = psuminf ?outer + e" 

636 
using psuminf_half_series by simp 

637 
finally show ?thesis . 

638 
qed 

639 
def C \<equiv> "(split BB) o prod_decode" 

640 
have C: "!!n. C n \<in> sets M" 

641 
apply (rule_tac p="prod_decode n" in PairE) 

642 
apply (simp add: C_def) 

643 
apply (metis BB subsetD rangeI) 

644 
done 

645 
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" 

646 
proof (auto simp add: C_def) 

647 
fix x i 

648 
assume x: "x \<in> A i" 

649 
with sbBB [of i] obtain j where "x \<in> BB i j" 

650 
by blast 

651 
thus "\<exists>i. x \<in> split BB (prod_decode i)" 

652 
by (metis prod_encode_inverse prod.cases) 

653 
qed 

654 
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode" 

655 
by (rule ext) (auto simp add: C_def) 

656 
moreover have "psuminf ... = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" using BBle 

657 
by (force intro!: psuminf_2dimen simp: o_def) 

658 
ultimately have Csums: "psuminf (f \<circ> C) = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" by simp 

659 
have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" 

660 
apply (rule inf_measure_le [OF posf(1) inc], auto) 

661 
apply (rule_tac x="C" in exI) 

662 
apply (auto simp add: C sbC Csums) 

663 
done 

664 
also have "... \<le> (\<Sum>\<^isub>\<infinity>n. Inf (measure_set M f (A n))) + e" using sll 

665 
by blast 

666 
finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> psuminf ?outer + e" . 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

667 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

668 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

669 
lemma (in algebra) inf_measure_outer: 
38656  670 
"\<lbrakk> positive f ; increasing M f \<rbrakk> 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

671 
\<Longrightarrow> outer_measure_space ( space = space M, sets = Pow (space M) ) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

672 
(\<lambda>x. Inf (measure_set M f x))" 
38656  673 
by (simp add: outer_measure_space_def inf_measure_empty 
674 
inf_measure_increasing inf_measure_countably_subadditive positive_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

675 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

676 
(*MOVE UP*) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

677 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

678 
lemma (in algebra) algebra_subset_lambda_system: 
38656  679 
assumes posf: "positive f" and inc: "increasing M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

680 
and add: "additive M f" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

681 
shows "sets M \<subseteq> lambda_system ( space = space M, sets = Pow (space M) ) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

682 
(\<lambda>x. Inf (measure_set M f x))" 
38656  683 
proof (auto dest: sets_into_space 
684 
simp add: algebra.lambda_system_eq [OF algebra_Pow]) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

685 
fix x s 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

686 
assume x: "x \<in> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

687 
and s: "s \<subseteq> space M" 
38656  688 
have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M  x) = sx" using s 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

689 
by blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

690 
have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx)) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

691 
\<le> Inf (measure_set M f s)" 
38656  692 
proof (rule pinfreal_le_epsilon) 
693 
fix e :: pinfreal 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

694 
assume e: "0 < e" 
38656  695 
from inf_measure_close [of f, OF posf e s] 
696 
obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A" 

697 
and sUN: "s \<subseteq> (\<Union>i. A i)" 

698 
and l: "psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e" 

33536  699 
by auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

700 
have [simp]: "!!x. x \<in> sets M \<Longrightarrow> 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

701 
(f o (\<lambda>z. z \<inter> (space M  x)) o A) = (f o (\<lambda>z. z  x) o A)" 
33536  702 
by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

703 
have [simp]: "!!n. f (A n \<inter> x) + f (A n  x) = f (A n)" 
33536  704 
by (subst additiveD [OF add, symmetric]) 
705 
(auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

706 
{ fix u 
33536  707 
assume u: "u \<in> sets M" 
38656  708 
have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)" 
709 
by (simp add: increasingD [OF inc] u Int range_subsetD [OF A]) 

710 
have 2: "Inf (measure_set M f (s \<inter> u)) \<le> psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A)" 

711 
proof (rule complete_lattice_class.Inf_lower) 

712 
show "psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)" 

713 
apply (simp add: measure_set_def) 

714 
apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) 

715 
apply (auto simp add: disjoint_family_subset [OF disj] o_def) 

716 
apply (blast intro: u range_subsetD [OF A]) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

717 
apply (blast dest: subsetD [OF sUN]) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

718 
done 
38656  719 
qed 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

720 
} note lesum = this 
38656  721 
have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> psuminf (f o (\<lambda>z. z\<inter>x) o A)" 
722 
and inf2: "Inf (measure_set M f (s \<inter> (space M  x))) 

723 
\<le> psuminf (f o (\<lambda>z. z \<inter> (space M  x)) o A)" 

33536  724 
by (metis Diff lesum top x)+ 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

725 
hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx)) 
38656  726 
\<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. sx) o A)" 
727 
by (simp add: x add_mono) 

728 
also have "... \<le> psuminf (f o A)" 

729 
by (simp add: x psuminf_add[symmetric] o_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

730 
also have "... \<le> Inf (measure_set M f s) + e" 
38656  731 
by (rule l) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

732 
finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx)) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

733 
\<le> Inf (measure_set M f s) + e" . 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

734 
qed 
38656  735 
moreover 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

736 
have "Inf (measure_set M f s) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

737 
\<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx))" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

738 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

739 
have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (sx)))" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

740 
by (metis Un_Diff_Int Un_commute) 
38656  741 
also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx))" 
742 
apply (rule subadditiveD) 

743 
apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 

33536  744 
inf_measure_positive inf_measure_countably_subadditive posf inc) 
38656  745 
apply (auto simp add: subsetD [OF s]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

746 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

747 
finally show ?thesis . 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

748 
qed 
38656  749 
ultimately 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

750 
show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx)) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

751 
= Inf (measure_set M f s)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

752 
by (rule order_antisym) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

753 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

754 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

755 
lemma measure_down: 
38656  756 
"measure_space N \<mu> \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow> 
757 
(\<nu> = \<mu>) \<Longrightarrow> measure_space M \<nu>" 

758 
by (simp add: measure_space_def measure_space_axioms_def positive_def 

759 
countably_additive_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

760 
blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

761 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

762 
theorem (in algebra) caratheodory: 
38656  763 
assumes posf: "positive f" and ca: "countably_additive M f" 
764 
shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma (space M) (sets M)) \<mu>" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

765 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

766 
have inc: "increasing M f" 
38656  767 
by (metis additive_increasing ca countably_additive_additive posf) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

768 
let ?infm = "(\<lambda>x. Inf (measure_set M f x))" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

769 
def ls \<equiv> "lambda_system (space = space M, sets = Pow (space M)) ?infm" 
38656  770 
have mls: "measure_space \<lparr>space = space M, sets = ls\<rparr> ?infm" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

771 
using sigma_algebra.caratheodory_lemma 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

772 
[OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

773 
by (simp add: ls_def) 
38656  774 
hence sls: "sigma_algebra (space = space M, sets = ls)" 
775 
by (simp add: measure_space_def) 

776 
have "sets M \<subseteq> ls" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

777 
by (simp add: ls_def) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

778 
(metis ca posf inc countably_additive_additive algebra_subset_lambda_system) 
38656  779 
hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

780 
using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

781 
by simp 
38656  782 
have "measure_space (sigma (space M) (sets M)) ?infm" 
783 
unfolding sigma_def 

784 
by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

785 
(simp_all add: sgs_sb space_closed) 
38656  786 
thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm]) 
787 
qed 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

788 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

789 
end 