author  haftmann 
Sat, 25 May 2013 15:44:29 +0200  
changeset 52141  eff000cab70f 
parent 51329  4a3c453f99a1 
child 55642  63beb38e9258 
permissions  rwrr 
42067  1 
(* Title: HOL/Probability/Caratheodory.thy 
2 
Author: Lawrence C Paulson 

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

4 
*) 

5 

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

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

7 

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

8 
theory Caratheodory 
47694  9 
imports Measure_Space 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

11 

42067  12 
text {* 
13 
Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson. 

14 
*} 

15 

43920  16 
lemma suminf_ereal_2dimen: 
17 
fixes f:: "nat \<times> nat \<Rightarrow> ereal" 

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

18 
assumes pos: "\<And>p. 0 \<le> f p" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

19 
assumes "\<And>m. g m = (\<Sum>n. f (m,n))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

20 
shows "(\<Sum>i. f (prod_decode i)) = suminf g" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

22 
have g_def: "g = (\<lambda>m. (\<Sum>n. f (m,n)))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

23 
using assms by (simp add: fun_eq_iff) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

24 
have reindex: "\<And>B. (\<Sum>x\<in>B. f (prod_decode x)) = setsum f (prod_decode ` B)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

25 
by (simp add: setsum_reindex[OF inj_prod_decode] comp_def) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

26 
{ fix n 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

27 
let ?M = "\<lambda>f. Suc (Max (f ` prod_decode ` {..<n}))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

28 
{ fix a b x assume "x < n" and [symmetric]: "(a, b) = prod_decode x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

29 
then have "a < ?M fst" "b < ?M snd" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

30 
by (auto intro!: Max_ge le_imp_less_Suc image_eqI) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

31 
then have "setsum f (prod_decode ` {..<n}) \<le> setsum f ({..<?M fst} \<times> {..<?M snd})" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

32 
by (auto intro!: setsum_mono3 simp: pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

33 
then have "\<exists>a b. setsum f (prod_decode ` {..<n}) \<le> setsum f ({..<a} \<times> {..<b})" by auto } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

35 
{ fix a b 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

36 
let ?M = "prod_decode ` {..<Suc (Max (prod_encode ` ({..<a} \<times> {..<b})))}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

37 
{ fix a' b' assume "a' < a" "b' < b" then have "(a', b') \<in> ?M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

38 
by (auto intro!: Max_ge le_imp_less_Suc image_eqI[where x="prod_encode (a', b')"]) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

39 
then have "setsum f ({..<a} \<times> {..<b}) \<le> setsum f ?M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

40 
by (auto intro!: setsum_mono3 simp: pos) } 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

42 
show ?thesis unfolding g_def using pos 
44928
7ef6505bde7f
renamed Complete_Lattices lemmas, removed legacy names
hoelzl
parents:
44918
diff
changeset

43 
by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex SUP_upper2 
43920  44 
setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair 
45 
SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg) 

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

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

47 

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

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

49 

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

50 
definition subadditive where "subadditive M f \<longleftrightarrow> 
47694  51 
(\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

52 

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

53 
definition countably_subadditive where "countably_subadditive M f \<longleftrightarrow> 
47694  54 
(\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

55 
(f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

56 

47694  57 
definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M. 
58 
\<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega>  l) \<inter> x) = f x}" 

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

59 

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

60 
definition outer_measure_space where "outer_measure_space M f \<longleftrightarrow> 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

61 
positive M f \<and> increasing M f \<and> countably_subadditive M f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

62 

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

63 
definition measure_set where "measure_set M f X = {r. 
47694  64 
\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

65 

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

66 
lemma subadditiveD: 
47694  67 
"subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

69 

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

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

71 

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

72 
lemma (in algebra) lambda_system_eq: 
47694  73 
shows "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x  l) = f x}" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

74 
proof  
47694  75 
have [simp]: "!!l x. l \<in> M \<Longrightarrow> x \<in> M \<Longrightarrow> (\<Omega>  l) \<inter> x = x  l" 
37032  76 
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

77 
show ?thesis 
37032  78 
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

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

80 

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

81 
lemma (in algebra) lambda_system_empty: 
47694  82 
"positive M f \<Longrightarrow> {} \<in> lambda_system \<Omega> M f" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

83 
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

84 

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

85 
lemma lambda_system_sets: 
47694  86 
"x \<in> lambda_system \<Omega> M f \<Longrightarrow> x \<in> M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

88 

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

89 
lemma (in algebra) lambda_system_Compl: 
43920  90 
fixes f:: "'a set \<Rightarrow> ereal" 
47694  91 
assumes x: "x \<in> lambda_system \<Omega> M f" 
92 
shows "\<Omega>  x \<in> lambda_system \<Omega> M f" 

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

93 
proof  
47694  94 
have "x \<subseteq> \<Omega>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

95 
by (metis sets_into_space lambda_system_sets x) 
47694  96 
hence "\<Omega>  (\<Omega>  x) = x" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

97 
by (metis double_diff equalityE) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

98 
with x show ?thesis 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

99 
by (force simp add: lambda_system_def ac_simps) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

101 

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

102 
lemma (in algebra) lambda_system_Int: 
43920  103 
fixes f:: "'a set \<Rightarrow> ereal" 
47694  104 
assumes xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" 
105 
shows "x \<inter> y \<in> lambda_system \<Omega> M f" 

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

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

107 
from xl yl show ?thesis 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

108 
proof (auto simp add: positive_def lambda_system_eq Int) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

109 
fix u 
47694  110 
assume x: "x \<in> M" and y: "y \<in> M" and u: "u \<in> M" 
111 
and fx: "\<forall>z\<in>M. f (z \<inter> x) + f (z  x) = f z" 

112 
and fy: "\<forall>z\<in>M. f (z \<inter> y) + f (z  y) = f z" 

113 
have "u  x \<inter> y \<in> M" 

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

114 
by (metis Diff Diff_Int Un u x y) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

116 
have "(u  (x \<inter> y)) \<inter> y = u \<inter> y  x" by blast 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

118 
have "u  x \<inter> y  y = u  y" by blast 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

120 
have ey: "f (u  x \<inter> y) = f (u \<inter> y  x) + f (u  y)" using fy 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

122 
have "f (u \<inter> (x \<inter> y)) + f (u  x \<inter> y) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

123 
= (f (u \<inter> (x \<inter> y)) + f (u \<inter> y  x)) + f (u  y)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

124 
by (simp add: ey ac_simps) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

125 
also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y  x)) + f (u  y)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

126 
by (simp add: Int_ac) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

127 
also have "... = f (u \<inter> y) + f (u  y)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

128 
using fx [THEN bspec, of "u \<inter> y"] Int y u 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

130 
also have "... = f u" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

131 
by (metis fy u) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

132 
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

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

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

135 

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

136 
lemma (in algebra) lambda_system_Un: 
43920  137 
fixes f:: "'a set \<Rightarrow> ereal" 
47694  138 
assumes xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" 
139 
shows "x \<union> y \<in> lambda_system \<Omega> M f" 

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

140 
proof  
47694  141 
have "(\<Omega>  x) \<inter> (\<Omega>  y) \<in> M" 
38656  142 
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

143 
moreover 
47694  144 
have "x \<union> y = \<Omega>  ((\<Omega>  x) \<inter> (\<Omega>  y))" 
46731  145 
by auto (metis subsetD lambda_system_sets sets_into_space xl yl)+ 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

146 
ultimately show ?thesis 
38656  147 
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

148 
qed 
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_algebra: 
47694  151 
"positive M f \<Longrightarrow> algebra \<Omega> (lambda_system \<Omega> M f)" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

152 
apply (auto simp add: algebra_iff_Un) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

153 
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

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

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

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

158 

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

159 
lemma (in algebra) lambda_system_strong_additive: 
47694  160 
assumes z: "z \<in> M" and disj: "x \<inter> y = {}" 
161 
and xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" 

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

162 
shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

164 
have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

166 
have "z \<inter> y = (z \<inter> (x \<union> y))  x" using disj by blast 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

167 
moreover 
47694  168 
have "(z \<inter> (x \<union> y)) \<in> M" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

169 
by (metis Int Un lambda_system_sets xl yl z) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

170 
ultimately show ?thesis using xl yl 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

171 
by (simp add: lambda_system_eq) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

173 

47694  174 
lemma (in algebra) lambda_system_additive: "additive (lambda_system \<Omega> M f) f" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

175 
proof (auto simp add: additive_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

176 
fix x and y 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

177 
assume disj: "x \<inter> y = {}" 
47694  178 
and xl: "x \<in> lambda_system \<Omega> M f" and yl: "y \<in> lambda_system \<Omega> M f" 
179 
hence "x \<in> M" "y \<in> M" by (blast intro: lambda_system_sets)+ 

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

180 
thus "f (x \<union> y) = f x + f y" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

181 
using lambda_system_strong_additive [OF top disj xl yl] 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

182 
by (simp add: Un) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

184 

42145  185 
lemma (in ring_of_sets) countably_subadditive_subadditive: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

186 
assumes f: "positive M f" and cs: "countably_subadditive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

191 
hence "disjoint_family (binaryset x y)" 
35582  192 
by (auto simp add: disjoint_family_on_def binaryset_def) 
47694  193 
hence "range (binaryset x y) \<subseteq> M \<longrightarrow> 
194 
(\<Union>i. binaryset x y i) \<in> M \<longrightarrow> 

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

195 
f (\<Union>i. binaryset x y i) \<le> (\<Sum> n. f (binaryset x y n))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

196 
using cs by (auto simp add: countably_subadditive_def) 
47694  197 
hence "{x,y,{}} \<subseteq> M \<longrightarrow> x \<union> y \<in> M \<longrightarrow> 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

199 
by (simp add: range_binaryset_eq UN_binaryset_eq) 
38656  200 
thus "f (x \<union> y) \<le> f x + f y" using f x y 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

201 
by (auto simp add: Un o_def suminf_binaryset_eq positive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

203 

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

204 
lemma lambda_system_increasing: 
47694  205 
"increasing M f \<Longrightarrow> increasing (lambda_system \<Omega> M f) f" 
38656  206 
by (simp add: increasing_def lambda_system_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

207 

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

208 
lemma lambda_system_positive: 
47694  209 
"positive M f \<Longrightarrow> positive (lambda_system \<Omega> M f) f" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

210 
by (simp add: positive_def lambda_system_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

211 

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

212 
lemma (in algebra) lambda_system_strong_sum: 
43920  213 
fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ereal" 
47694  214 
assumes f: "positive M f" and a: "a \<in> M" 
215 
and A: "range A \<subseteq> lambda_system \<Omega> M f" 

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

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

217 
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

218 
proof (induct n) 
38656  219 
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

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

222 
have 2: "A n \<inter> UNION {0..<n} A = {}" using disj 
38656  223 
by (force simp add: disjoint_family_on_def neq_iff) 
47694  224 
have 3: "A n \<in> lambda_system \<Omega> M f" using A 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

225 
by blast 
47694  226 
interpret l: algebra \<Omega> "lambda_system \<Omega> M f" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

227 
using f by (rule lambda_system_algebra) 
47694  228 
have 4: "UNION {0..<n} A \<in> lambda_system \<Omega> M f" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

229 
using A l.UNION_in_sets by simp 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

231 
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

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

233 

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

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

235 
assumes oms: "outer_measure_space M f" 
47694  236 
and A: "range A \<subseteq> lambda_system \<Omega> M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

237 
and disj: "disjoint_family A" 
47694  238 
shows "(\<Union>i. A i) \<in> lambda_system \<Omega> M f \<and> (\<Sum>i. f (A i)) = f (\<Union>i. A i)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

240 
have pos: "positive M f" and inc: "increasing M f" 
38656  241 
and csa: "countably_subadditive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

243 
have sa: "subadditive M f" 
38656  244 
by (metis countably_subadditive_subadditive csa pos) 
47694  245 
have A': "\<And>S. A`S \<subseteq> (lambda_system \<Omega> M f)" using A 
246 
by auto 

247 
interpret ls: algebra \<Omega> "lambda_system \<Omega> M f" 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

248 
using pos by (rule lambda_system_algebra) 
47694  249 
have A'': "range A \<subseteq> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

250 
by (metis A image_subset_iff lambda_system_sets) 
38656  251 

47694  252 
have U_in: "(\<Union>i. A i) \<in> M" 
37032  253 
by (metis A'' countable_UN) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

254 
have U_eq: "f (\<Union>i. A i) = (\<Sum>i. f (A i))" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

255 
proof (rule antisym) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

256 
show "f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

257 
using csa[unfolded countably_subadditive_def] A'' disj U_in by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

258 
have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

259 
have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

260 
show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

261 
using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis] 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

262 
using A'' 
47694  263 
by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] countable_UN) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

265 
{ 
38656  266 
fix a 
47694  267 
assume a [iff]: "a \<in> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

268 
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

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

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

271 
proof (rule antisym) 
47694  272 
have "range (\<lambda>i. a \<inter> A i) \<subseteq> M" using A'' 
33536  273 
by blast 
38656  274 
moreover 
33536  275 
have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj 
38656  276 
by (auto simp add: disjoint_family_on_def) 
277 
moreover 

47694  278 
have "a \<inter> (\<Union>i. A i) \<in> M" 
33536  279 
by (metis Int U_in a) 
38656  280 
ultimately 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

281 
have "f (a \<inter> (\<Union>i. A i)) \<le> (\<Sum>i. f (a \<inter> A i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

282 
using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"] 
38656  283 
by (simp add: o_def) 
284 
hence "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) \<le> 

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

285 
(\<Sum>i. f (a \<inter> A i)) + f (a  (\<Union>i. A i))" 
38656  286 
by (rule add_right_mono) 
287 
moreover 

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

288 
have "(\<Sum>i. f (a \<inter> A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

289 
proof (intro suminf_bound_add allI) 
33536  290 
fix n 
47694  291 
have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> M" 
38656  292 
by (metis A'' UNION_in_sets) 
33536  293 
have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' 
37032  294 
by (blast intro: increasingD [OF inc] A'' UNION_in_sets) 
47694  295 
have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system \<Omega> M f" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

296 
using ls.UNION_in_sets by (simp add: A) 
38656  297 
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  298 
by (simp add: lambda_system_eq UNION_in) 
33536  299 
have "f (a  (\<Union>i. A i)) \<le> f (a  (\<Union>i\<in>{0..<n}. A i))" 
44106  300 
by (blast intro: increasingD [OF inc] UNION_in U_in) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

301 
thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
38656  302 
by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

303 
next 
47694  304 
have "\<And>i. a \<inter> A i \<in> M" using A'' by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

305 
then show "\<And>i. 0 \<le> f (a \<inter> A i)" using pos[unfolded positive_def] by auto 
47694  306 
have "\<And>i. a  (\<Union>i. A i) \<in> M" using A'' by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

307 
then have "\<And>i. 0 \<le> f (a  (\<Union>i. A i))" using pos[unfolded positive_def] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

308 
then show "f (a  (\<Union>i. A i)) \<noteq> \<infinity>" by auto 
33536  309 
qed 
38656  310 
ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
311 
by (rule order_trans) 

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

312 
next 
38656  313 
have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a  (\<Union>i. A i)))" 
37032  314 
by (blast intro: increasingD [OF inc] U_in) 
33536  315 
also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i))" 
37032  316 
by (blast intro: subadditiveD [OF sa] U_in) 
33536  317 
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

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

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

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

321 
thus ?thesis 
38656  322 
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

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

324 

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

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

326 
assumes oms: "outer_measure_space M f" 
47694  327 
defines "L \<equiv> lambda_system \<Omega> M f" 
328 
shows "measure_space \<Omega> L f" 

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

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

330 
have pos: "positive M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

331 
by (metis oms outer_measure_space_def) 
47694  332 
have alg: "algebra \<Omega> L" 
38656  333 
using lambda_system_algebra [of f, OF pos] 
47694  334 
by (simp add: algebra_iff_Un L_def) 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

335 
then 
47694  336 
have "sigma_algebra \<Omega> L" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

337 
using lambda_system_caratheodory [OF oms] 
47694  338 
by (simp add: sigma_algebra_disjoint_iff L_def) 
38656  339 
moreover 
47694  340 
have "countably_additive L f" "positive L f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

341 
using pos lambda_system_caratheodory [OF oms] 
47694  342 
by (auto simp add: lambda_system_sets L_def countably_additive_def positive_def) 
38656  343 
ultimately 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

344 
show ?thesis 
47694  345 
using pos by (simp add: measure_space_def) 
38656  346 
qed 
347 

39096  348 
lemma inf_measure_nonempty: 
47694  349 
assumes f: "positive M f" and b: "b \<in> M" and a: "a \<subseteq> b" "{} \<in> M" 
39096  350 
shows "f b \<in> measure_set M f a" 
351 
proof  

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

352 
let ?A = "\<lambda>i::nat. (if i = 0 then b else {})" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

353 
have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))" 
47761  354 
by (rule suminf_finite) (simp_all add: f[unfolded positive_def]) 
39096  355 
also have "... = f b" 
356 
by simp 

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

357 
finally show ?thesis using assms 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

358 
by (auto intro!: exI [of _ ?A] 
39096  359 
simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) 
360 
qed 

361 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

362 
lemma (in ring_of_sets) inf_measure_agrees: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

363 
assumes posf: "positive M f" and ca: "countably_additive M f" 
47694  364 
and s: "s \<in> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

365 
shows "Inf (measure_set M f s) = f s" 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
49773
diff
changeset

366 
proof (intro Inf_eqI) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

368 
assume z: "z \<in> measure_set M f s" 
38656  369 
from this obtain A where 
47694  370 
A: "range A \<subseteq> M" and disj: "disjoint_family A" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

371 
and "s \<subseteq> (\<Union>x. A x)" and si: "(\<Sum>i. f (A i)) = z" 
38656  372 
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

373 
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

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

375 
by (metis additive_increasing ca countably_additive_additive posf) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

376 
have sums: "(\<Sum>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

377 
proof (rule ca[unfolded countably_additive_def, rule_format]) 
47694  378 
show "range (\<lambda>n. A n \<inter> s) \<subseteq> M" using A s 
33536  379 
by blast 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

380 
show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj 
35582  381 
by (auto simp add: disjoint_family_on_def) 
47694  382 
show "(\<Union>i. A i \<inter> s) \<in> M" using A s 
33536  383 
by (metis UN_extend_simps(4) s seq) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

385 
hence "f s = (\<Sum>i. f (A i \<inter> s))" 
37032  386 
using seq [symmetric] by (simp add: sums_iff) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

387 
also have "... \<le> (\<Sum>i. f (A i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

388 
proof (rule suminf_le_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

389 
fix n show "f (A n \<inter> s) \<le> f (A n)" using A s 
38656  390 
by (force intro: increasingD [OF inc]) 
47694  391 
fix N have "A N \<inter> s \<in> M" using A s by auto 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

392 
then show "0 \<le> f (A N \<inter> s)" using posf unfolding positive_def by auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

395 
finally show "f s \<le> z" . 
51329
4a3c453f99a1
split dense into inner_dense_order and no_top/no_bot
hoelzl
parents:
49773
diff
changeset

396 
qed (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

397 

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

398 
lemma measure_set_pos: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

399 
assumes posf: "positive M f" "r \<in> measure_set M f X" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

400 
shows "0 \<le> r" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

401 
proof  
47694  402 
obtain A where "range A \<subseteq> M" and r: "r = (\<Sum>i. f (A i))" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

403 
using `r \<in> measure_set M f X` unfolding measure_set_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

404 
then show "0 \<le> r" using posf unfolding r positive_def 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

405 
by (intro suminf_0_le) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

407 

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

408 
lemma inf_measure_pos: 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

409 
assumes posf: "positive M f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

410 
shows "0 \<le> Inf (measure_set M f X)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

411 
proof (rule complete_lattice_class.Inf_greatest) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

412 
fix r assume "r \<in> measure_set M f X" with posf show "0 \<le> r" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

413 
by (rule measure_set_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

415 

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

416 
lemma inf_measure_empty: 
47694  417 
assumes posf: "positive M f" and "{} \<in> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

420 
show "Inf (measure_set M f {}) \<le> 0" 
47694  421 
by (metis complete_lattice_class.Inf_lower `{} \<in> M` 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

422 
inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

423 
qed (rule inf_measure_pos[OF posf]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

424 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

425 
lemma (in ring_of_sets) inf_measure_positive: 
47694  426 
assumes p: "positive M f" and "{} \<in> M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

427 
shows "positive M (\<lambda>x. Inf (measure_set M f x))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

428 
proof (unfold positive_def, intro conjI ballI) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

429 
show "Inf (measure_set M f {}) = 0" using inf_measure_empty[OF assms] by auto 
47694  430 
fix A assume "A \<in> M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

431 
qed (rule inf_measure_pos[OF p]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

432 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

433 
lemma (in ring_of_sets) inf_measure_increasing: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

434 
assumes posf: "positive M f" 
47694  435 
shows "increasing (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" 
44918  436 
apply (clarsimp simp add: increasing_def) 
38656  437 
apply (rule complete_lattice_class.Inf_greatest) 
438 
apply (rule complete_lattice_class.Inf_lower) 

37032  439 
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

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

441 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

442 
lemma (in ring_of_sets) inf_measure_le: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

443 
assumes posf: "positive M f" and inc: "increasing M f" 
47694  444 
and x: "x \<in> {r . \<exists>A. range A \<subseteq> M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

446 
proof  
47694  447 
obtain A where A: "range A \<subseteq> M" and ss: "s \<subseteq> (\<Union>i. A i)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

448 
and xeq: "(\<Sum>i. f (A i)) = x" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

449 
using x by auto 
47694  450 
have dA: "range (disjointed A) \<subseteq> M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

451 
by (metis A range_disjointed_sets) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

452 
have "\<forall>n. f (disjointed A n) \<le> f (A n)" 
38656  453 
by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

454 
moreover have "\<forall>i. 0 \<le> f (disjointed A i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

455 
using posf dA unfolding positive_def by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

456 
ultimately have sda: "(\<Sum>i. f (disjointed A i)) \<le> (\<Sum>i. f (A i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

457 
by (blast intro!: suminf_le_pos) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

458 
hence ley: "(\<Sum>i. f (disjointed A i)) \<le> x" 
38656  459 
by (metis xeq) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

460 
hence y: "(\<Sum>i. f (disjointed A i)) \<in> measure_set M f s" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

461 
apply (auto simp add: measure_set_def) 
38656  462 
apply (rule_tac x="disjointed A" in exI) 
463 
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

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

465 
show ?thesis 
38656  466 
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

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

468 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

469 
lemma (in ring_of_sets) inf_measure_close: 
43920  470 
fixes e :: ereal 
47694  471 
assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (\<Omega>)" and "Inf (measure_set M f s) \<noteq> \<infinity>" 
472 
shows "\<exists>A. range A \<subseteq> M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and> 

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

473 
(\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

474 
proof  
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

475 
from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

476 
using inf_measure_pos[OF posf, of s] by auto 
38656  477 
obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e" 
43920  478 
using Inf_ereal_close[OF fin e] by auto 
38656  479 
thus ?thesis 
480 
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

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

482 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

483 
lemma (in ring_of_sets) inf_measure_countably_subadditive: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

484 
assumes posf: "positive M f" and inc: "increasing M f" 
47694  485 
shows "countably_subadditive (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

486 
proof (simp add: countably_subadditive_def, safe) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

487 
fix A :: "nat \<Rightarrow> 'a set" 
46731  488 
let ?outer = "\<lambda>B. Inf (measure_set M f B)" 
47694  489 
assume A: "range A \<subseteq> Pow (\<Omega>)" 
38656  490 
and disj: "disjoint_family A" 
47694  491 
and sb: "(\<Union>i. A i) \<subseteq> \<Omega>" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

492 

43920  493 
{ fix e :: ereal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>" 
47694  494 
hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> M \<and> disjoint_family (BB n) \<and> 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

495 
A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

496 
apply (safe intro!: choice inf_measure_close [of f, OF posf]) 
43920  497 
using e sb by (auto simp: ereal_zero_less_0_iff one_ereal_def) 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

498 
then obtain BB 
47694  499 
where BB: "\<And>n. (range (BB n) \<subseteq> M)" 
38656  500 
and disjBB: "\<And>n. disjoint_family (BB n)" 
501 
and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)" 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

502 
and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

503 
by auto blast 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

504 
have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e" 
38656  505 
proof  
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

506 
have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e" 
43920  507 
using suminf_half_series_ereal e 
508 
by (simp add: ereal_zero_le_0_iff zero_le_divide_ereal suminf_cmult_ereal) 

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

509 
have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

510 
then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le) 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

511 
then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

512 
by (rule suminf_le_pos[OF BBle]) 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

513 
also have "... = (\<Sum>n. ?outer (A n)) + e" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

514 
using sum_eq_1 inf_measure_pos[OF posf] e 
43920  515 
by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff) 
38656  516 
finally show ?thesis . 
517 
qed 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

518 
def C \<equiv> "(split BB) o prod_decode" 
47694  519 
have C: "!!n. C n \<in> M" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

520 
apply (rule_tac p="prod_decode n" in PairE) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

521 
apply (simp add: C_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

522 
apply (metis BB subsetD rangeI) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

523 
done 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

524 
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" 
38656  525 
proof (auto simp add: C_def) 
526 
fix x i 

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

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

529 
by blast 

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

531 
by (metis prod_encode_inverse prod.cases) 

532 
qed 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

533 
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

534 
by (rule ext) (auto simp add: C_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

535 
moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

536 
using BB posf[unfolded positive_def] 
43920  537 
by (force intro!: suminf_ereal_2dimen simp: o_def) 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

538 
ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

539 
have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

540 
apply (rule inf_measure_le [OF posf(1) inc], auto) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

541 
apply (rule_tac x="C" in exI) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

542 
apply (auto simp add: C sbC Csums) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

543 
done 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

544 
also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

545 
by blast 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

546 
finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . } 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

547 
note for_finite_Inf = this 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

548 

6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

549 
show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

550 
proof cases 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

551 
assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

552 
with for_finite_Inf show ?thesis 
43920  553 
by (intro ereal_le_epsilon) auto 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

554 
next 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

555 
assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

556 
then have "\<exists>i. ?outer (A i) = \<infinity>" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

557 
by auto 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

558 
then have "(\<Sum>n. ?outer (A n)) = \<infinity>" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

559 
using suminf_PInfty[OF inf_measure_pos, OF posf] 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

560 
by metis 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

561 
then show ?thesis by simp 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

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

564 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

565 
lemma (in ring_of_sets) inf_measure_outer: 
47694  566 
"\<lbrakk> positive M f ; increasing M f \<rbrakk> \<Longrightarrow> 
567 
outer_measure_space (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" 

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

568 
using inf_measure_pos[of M f] 
38656  569 
by (simp add: outer_measure_space_def inf_measure_empty 
570 
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

571 

42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

572 
lemma (in ring_of_sets) algebra_subset_lambda_system: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

573 
assumes posf: "positive M f" and inc: "increasing M f" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

574 
and add: "additive M f" 
47694  575 
shows "M \<subseteq> lambda_system \<Omega> (Pow \<Omega>) (\<lambda>x. Inf (measure_set M f x))" 
38656  576 
proof (auto dest: sets_into_space 
577 
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

578 
fix x s 
47694  579 
assume x: "x \<in> M" 
580 
and s: "s \<subseteq> \<Omega>" 

581 
have [simp]: "!!x. x \<in> M \<Longrightarrow> s \<inter> (\<Omega>  x) = sx" using s 

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

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

583 
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

584 
\<le> Inf (measure_set M f s)" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

585 
proof cases 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

586 
assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

587 
next 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

588 
assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

589 
then have "measure_set M f s \<noteq> {}" 
43920  590 
by (auto simp: top_ereal_def) 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

591 
show ?thesis 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

592 
proof (rule complete_lattice_class.Inf_greatest) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

593 
fix r assume "r \<in> measure_set M f s" 
47694  594 
then obtain A where A: "disjoint_family A" "range A \<subseteq> M" "s \<subseteq> (\<Union>i. A i)" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

595 
and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

596 
have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

597 
unfolding measure_set_def 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

598 
proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"]) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

599 
from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

600 
by (rule disjoint_family_on_bisimulation) auto 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

601 
qed (insert x A, auto) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

602 
moreover 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

603 
have "Inf (measure_set M f (s  x)) \<le> (\<Sum>i. f (A i  x))" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

604 
unfolding measure_set_def 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

605 
proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i  x"]) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

606 
from A(1) show "disjoint_family (\<lambda>i. A i  x)" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

607 
by (rule disjoint_family_on_bisimulation) auto 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

608 
qed (insert x A, auto) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

609 
ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s  x)) \<le> 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

610 
(\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i  x))" by (rule add_mono) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

611 
also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i  x))" 
43920  612 
using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def) 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

613 
also have "\<dots> = (\<Sum>i. f (A i))" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

614 
using A x 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

615 
by (subst add[THEN additiveD, symmetric]) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

616 
(auto intro!: arg_cong[where f=suminf] arg_cong[where f=f]) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

617 
finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s  x)) \<le> r" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

618 
using r by simp 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

619 
qed 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

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

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

625 
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

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

42145  629 
apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow]) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

630 
apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf]) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

631 
apply (rule inf_measure_countably_subadditive) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

632 
using s by (auto intro!: posf inc) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

633 
finally show ?thesis . 
42145  634 
qed 
38656  635 
ultimately 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

636 
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

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

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

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

640 

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

641 
lemma measure_down: 
47694  642 
"measure_space \<Omega> N \<mu> \<Longrightarrow> sigma_algebra \<Omega> M \<Longrightarrow> M \<subseteq> N \<Longrightarrow> measure_space \<Omega> M \<mu>" 
643 
by (simp add: measure_space_def positive_def countably_additive_def) 

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

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

645 

47762  646 
theorem (in ring_of_sets) caratheodory': 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

647 
assumes posf: "positive M f" and ca: "countably_additive M f" 
47694  648 
shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

650 
have inc: "increasing M f" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

651 
by (metis additive_increasing ca countably_additive_additive posf) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

652 
let ?infm = "(\<lambda>x. Inf (measure_set M f x))" 
47694  653 
def ls \<equiv> "lambda_system \<Omega> (Pow \<Omega>) ?infm" 
654 
have mls: "measure_space \<Omega> ls ?infm" 

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

655 
using sigma_algebra.caratheodory_lemma 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

656 
[OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

657 
by (simp add: ls_def) 
47694  658 
hence sls: "sigma_algebra \<Omega> ls" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

659 
by (simp add: measure_space_def) 
47694  660 
have "M \<subseteq> ls" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

661 
by (simp add: ls_def) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

662 
(metis ca posf inc countably_additive_additive algebra_subset_lambda_system) 
47694  663 
hence sgs_sb: "sigma_sets (\<Omega>) (M) \<subseteq> ls" 
664 
using sigma_algebra.sigma_sets_subset [OF sls, of "M"] 

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

665 
by simp 
47694  666 
have "measure_space \<Omega> (sigma_sets \<Omega> M) ?infm" 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

667 
by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

668 
(simp_all add: sgs_sb space_closed) 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

669 
thus ?thesis using inf_measure_agrees [OF posf ca] 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

670 
by (intro exI[of _ ?infm]) auto 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41023
diff
changeset

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

672 

42145  673 
subsubsection {*Alternative instances of caratheodory*} 
674 

675 
lemma (in ring_of_sets) caratheodory_empty_continuous: 

47694  676 
assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>" 
677 
assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) > 0" 

678 
shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>" 

47762  679 
proof (intro caratheodory' empty_continuous_imp_countably_additive f) 
47694  680 
show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto 
42145  681 
qed (rule cont) 
682 

47762  683 
section {* Volumes *} 
684 

685 
definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where 

686 
"volume M f \<longleftrightarrow> 

687 
(f {} = 0) \<and> (\<forall>a\<in>M. 0 \<le> f a) \<and> 

688 
(\<forall>C\<subseteq>M. disjoint C \<longrightarrow> finite C \<longrightarrow> \<Union>C \<in> M \<longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c))" 

689 

690 
lemma volumeI: 

691 
assumes "f {} = 0" 

692 
assumes "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> f a" 

693 
assumes "\<And>C. C \<subseteq> M \<Longrightarrow> disjoint C \<Longrightarrow> finite C \<Longrightarrow> \<Union>C \<in> M \<Longrightarrow> f (\<Union>C) = (\<Sum>c\<in>C. f c)" 

694 
shows "volume M f" 

695 
using assms by (auto simp: volume_def) 

696 

697 
lemma volume_positive: 

698 
"volume M f \<Longrightarrow> a \<in> M \<Longrightarrow> 0 \<le> f a" 

699 
by (auto simp: volume_def) 

700 

701 
lemma volume_empty: 

702 
"volume M f \<Longrightarrow> f {} = 0" 

703 
by (auto simp: volume_def) 

704 

705 
lemma volume_finite_additive: 

706 
assumes "volume M f" 

707 
assumes A: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> M" "disjoint_family_on A I" "finite I" "UNION I A \<in> M" 

708 
shows "f (UNION I A) = (\<Sum>i\<in>I. f (A i))" 

709 
proof  

52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51329
diff
changeset

710 
have "A`I \<subseteq> M" "disjoint (A`I)" "finite (A`I)" "\<Union>(A`I) \<in> M" 
47762  711 
using A unfolding SUP_def by (auto simp: disjoint_family_on_disjoint_image) 
52141
eff000cab70f
weaker precendence of syntax for big intersection and union on sets
haftmann
parents:
51329
diff
changeset

712 
with `volume M f` have "f (\<Union>(A`I)) = (\<Sum>a\<in>A`I. f a)" 
47762  713 
unfolding volume_def by blast 
714 
also have "\<dots> = (\<Sum>i\<in>I. f (A i))" 

715 
proof (subst setsum_reindex_nonzero) 

716 
fix i j assume "i \<in> I" "j \<in> I" "i \<noteq> j" "A i = A j" 

717 
with `disjoint_family_on A I` have "A i = {}" 

718 
by (auto simp: disjoint_family_on_def) 

719 
then show "f (A i) = 0" 

720 
using volume_empty[OF `volume M f`] by simp 

721 
qed (auto intro: `finite I`) 

722 
finally show "f (UNION I A) = (\<Sum>i\<in>I. f (A i))" 

723 
by simp 

724 
qed 

725 

726 
lemma (in ring_of_sets) volume_additiveI: 

727 
assumes pos: "\<And>a. a \<in> M \<Longrightarrow> 0 \<le> \<mu> a" 

728 
assumes [simp]: "\<mu> {} = 0" 

729 
assumes add: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> M \<Longrightarrow> a \<inter> b = {} \<Longrightarrow> \<mu> (a \<union> b) = \<mu> a + \<mu> b" 

730 
shows "volume M \<mu>" 

731 
proof (unfold volume_def, safe) 

732 
fix C assume "finite C" "C \<subseteq> M" "disjoint C" 

733 
then show "\<mu> (\<Union>C) = setsum \<mu> C" 

734 
proof (induct C) 

735 
case (insert c C) 

736 
from insert(1,2,4,5) have "\<mu> (\<Union>insert c C) = \<mu> c + \<mu> (\<Union>C)" 

737 
by (auto intro!: add simp: disjoint_def) 

738 
with insert show ?case 

739 
by (simp add: disjoint_def) 

740 
qed simp 

741 
qed fact+ 

742 

743 
lemma (in semiring_of_sets) extend_volume: 

744 
assumes "volume M \<mu>" 

745 
shows "\<exists>\<mu>'. volume generated_ring \<mu>' \<and> (\<forall>a\<in>M. \<mu>' a = \<mu> a)" 

746 
proof  

747 
let ?R = generated_ring 

748 
have "\<forall>a\<in>?R. \<exists>m. \<exists>C\<subseteq>M. a = \<Union>C \<and> finite C \<and> disjoint C \<and> m = (\<Sum>c\<in>C. \<mu> c)" 

749 
by (auto simp: generated_ring_def) 

750 
from bchoice[OF this] guess \<mu>' .. note \<mu>'_spec = this 

751 

752 
{ fix C assume C: "C \<subseteq> M" "finite C" "disjoint C" 

753 
fix D assume D: "D \<subseteq> M" "finite D" "disjoint D" 

754 
assume "\<Union>C = \<Union>D" 

755 
have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>d\<in>D. \<Sum>c\<in>C. \<mu> (c \<inter> d))" 

756 
proof (intro setsum_cong refl) 

757 
fix d assume "d \<in> D" 

758 
have Un_eq_d: "(\<Union>c\<in>C. c \<inter> d) = d" 

759 
using `d \<in> D` `\<Union>C = \<Union>D` by auto 

760 
moreover have "\<mu> (\<Union>c\<in>C. c \<inter> d) = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" 

761 
proof (rule volume_finite_additive) 

762 
{ fix c assume "c \<in> C" then show "c \<inter> d \<in> M" 

763 
using C D `d \<in> D` by auto } 

764 
show "(\<Union>a\<in>C. a \<inter> d) \<in> M" 

765 
unfolding Un_eq_d using `d \<in> D` D by auto 

766 
show "disjoint_family_on (\<lambda>a. a \<inter> d) C" 

767 
using `disjoint C` by (auto simp: disjoint_family_on_def disjoint_def) 

768 
qed fact+ 

769 
ultimately show "\<mu> d = (\<Sum>c\<in>C. \<mu> (c \<inter> d))" by simp 

770 
qed } 

771 
note split_sum = this 

772 

773 
{ fix C assume C: "C \<subseteq> M" "finite C" "disjoint C" 

774 
fix D assume D: "D \<subseteq> M" "finite D" "disjoint D" 

775 
assume "\<Union>C = \<Union>D" 

776 
with split_sum[OF C D] split_sum[OF D C] 

777 
have "(\<Sum>d\<in>D. \<mu> d) = (\<Sum>c\<in>C. \<mu> c)" 

778 
by (simp, subst setsum_commute, simp add: ac_simps) } 

779 
note sum_eq = this 

780 

781 
{ fix C assume C: "C \<subseteq> M" "finite C" "disjoint C" 

782 
then have "\<Union>C \<in> ?R" by (auto simp: generated_ring_def) 

783 
with \<mu>'_spec[THEN bspec, of "\<Union>C"] 

784 
obtain D where 

785 
D: "D \<subseteq> M" "finite D" "disjoint D" "\<Union>C = \<Union>D" and "\<mu>' (\<Union>C) = (\<Sum>d\<in>D. \<mu> d)" 

786 
by blast 

787 
with sum_eq[OF C D] have "\<mu>' (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" by simp } 

788 
note \<mu>' = this 

789 

790 
show ?thesis 

791 
proof (intro exI conjI ring_of_sets.volume_additiveI[OF generating_ring] ballI) 

792 
fix a assume "a \<in> M" with \<mu>'[of "{a}"] show "\<mu>' a = \<mu> a" 

793 
by (simp add: disjoint_def) 

794 
next 

795 
fix a assume "a \<in> ?R" then guess Ca .. note Ca = this 

796 
with \<mu>'[of Ca] `volume M \<mu>`[THEN volume_positive] 

797 
show "0 \<le> \<mu>' a" 

798 
by (auto intro!: setsum_nonneg) 

799 
next 

800 
show "\<mu>' {} = 0" using \<mu>'[of "{}"] by auto 

801 
next 

802 
fix a assume "a \<in> ?R" then guess Ca .. note Ca = this 

803 
fix b assume "b \<in> ?R" then guess Cb .. note Cb = this 

804 
assume "a \<inter> b = {}" 

805 
with Ca Cb have "Ca \<inter> Cb \<subseteq> {{}}" by auto 

806 
then have C_Int_cases: "Ca \<inter> Cb = {{}} \<or> Ca \<inter> Cb = {}" by auto 

807 

808 
from `a \<inter> b = {}` have "\<mu>' (\<Union> (Ca \<union> Cb)) = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c)" 

809 
using Ca Cb by (intro \<mu>') (auto intro!: disjoint_union) 

810 
also have "\<dots> = (\<Sum>c\<in>Ca \<union> Cb. \<mu> c) + (\<Sum>c\<in>Ca \<inter> Cb. \<mu> c)" 

811 
using C_Int_cases volume_empty[OF `volume M \<mu>`] by (elim disjE) simp_all 

812 
also have "\<dots> = (\<Sum>c\<in>Ca. \<mu> c) + (\<Sum>c\<in>Cb. \<mu> c)" 

813 
using Ca Cb by (simp add: setsum_Un_Int) 

814 
also have "\<dots> = \<mu>' a + \<mu>' b" 

815 
using Ca Cb by (simp add: \<mu>') 

816 
finally show "\<mu>' (a \<union> b) = \<mu>' a + \<mu>' b" 

817 
using Ca Cb by simp 

818 
qed 

819 
qed 

820 

821 
section {* Caratheodory on semirings *} 

822 

823 
theorem (in semiring_of_sets) caratheodory: 

824 
assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>" 

825 
shows "\<exists>\<mu>' :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu>' s = \<mu> s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>'" 

826 
proof  

827 
have "volume M \<mu>" 

828 
proof (rule volumeI) 

829 
{ fix a assume "a \<in> M" then show "0 \<le> \<mu> a" 

830 
using pos unfolding positive_def by auto } 

831 
note p = this 

832 

833 
fix C assume sets_C: "C \<subseteq> M" "\<Union>C \<in> M" and "disjoint C" "finite C" 

834 
have "\<exists>F'. bij_betw F' {..<card C} C" 

835 
by (rule finite_same_card_bij[OF _ `finite C`]) auto 

836 
then guess F' .. note F' = this 

837 
then have F': "C = F' ` {..< card C}" "inj_on F' {..< card C}" 

838 
by (auto simp: bij_betw_def) 

839 
{ fix i j assume *: "i < card C" "j < card C" "i \<noteq> j" 

840 
with F' have "F' i \<in> C" "F' j \<in> C" "F' i \<noteq> F' j" 

841 
unfolding inj_on_def by auto 

842 
with `disjoint C`[THEN disjointD] 

843 
have "F' i \<inter> F' j = {}" 

844 
by auto } 

845 
note F'_disj = this 

846 
def F \<equiv> "\<lambda>i. if i < card C then F' i else {}" 

847 
then have "disjoint_family F" 

848 
using F'_disj by (auto simp: disjoint_family_on_def) 

849 
moreover from F' have "(\<Union>i. F i) = \<Union>C" 

850 
by (auto simp: F_def set_eq_iff split: split_if_asm) 

851 
moreover have sets_F: "\<And>i. F i \<in> M" 

852 
using F' sets_C by (auto simp: F_def) 

853 
moreover note sets_C 

854 
ultimately have "\<mu> (\<Union>C) = (\<Sum>i. \<mu> (F i))" 

855 
using ca[unfolded countably_additive_def, THEN spec, of F] by auto 

856 
also have "\<dots> = (\<Sum>i<card C. \<mu> (F' i))" 

857 
proof  

858 
have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) sums (\<Sum>i<card C. \<mu> (F' i))" 

859 
by (rule sums_If_finite_set) auto 

860 
also have "(\<lambda>i. if i \<in> {..< card C} then \<mu> (F' i) else 0) = (\<lambda>i. \<mu> (F i))" 

861 
using pos by (auto simp: positive_def F_def) 

862 
finally show "(\<Sum>i. \<mu> (F i)) = (\<Sum>i<card C. \<mu> (F' i))" 

863 
by (simp add: sums_iff) 

864 
qed 

865 
also have "\<dots> = (\<Sum>c\<in>C. \<mu> c)" 

866 
using F'(2) by (subst (2) F') (simp add: setsum_reindex) 

867 
finally show "\<mu> (\<Union>C) = (\<Sum>c\<in>C. \<mu> c)" . 

868 
next 

869 
show "\<mu> {} = 0" 

870 
using `positive M \<mu>` by (rule positiveD1) 

871 
qed 

872 
from extend_volume[OF this] obtain \<mu>_r where 

873 
V: "volume generated_ring \<mu>_r" "\<And>a. a \<in> M \<Longrightarrow> \<mu> a = \<mu>_r a" 

874 
by auto 

875 

876 
interpret G: ring_of_sets \<Omega> generated_ring 

877 
by (rule generating_ring) 

878 

879 
have pos: "positive generated_ring \<mu>_r" 

880 
using V unfolding positive_def by (auto simp: positive_def intro!: volume_positive volume_empty) 

881 

882 
have "countably_additive generated_ring \<mu>_r" 

883 
proof (rule countably_additiveI) 

884 
fix A' :: "nat \<Rightarrow> 'a set" assume A': "range A' \<subseteq> generated_ring" "disjoint_family A'" 

885 
and Un_A: "(\<Union>i. A' i) \<in> generated_ring" 

886 

887 
from generated_ringE[OF Un_A] guess C' . note C' = this 

888 

889 
{ fix c assume "c \<in> C'" 

890 
moreover def A \<equiv> "\<lambda>i. A' i \<inter> c" 

891 
ultimately have A: "range A \<subseteq> generated_ring" "disjoint_family A" 

892 
and Un_A: "(\<Union>i. A i) \<in> generated_ring" 

893 
using A' C' 

894 
by (auto intro!: G.Int G.finite_Union intro: generated_ringI_Basic simp: disjoint_family_on_def) 

895 
from A C' `c \<in> C'` have UN_eq: "(\<Union>i. A i) = c" 

896 
by (auto simp: A_def) 

897 

898 
have "\<forall>i::nat. \<exists>f::nat \<Rightarrow> 'a set. \<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j)) \<and> disjoint_family f \<and> \<Union>range f = A i \<and> (\<forall>j. f j \<in> M)" 

899 
(is "\<forall>i. ?P i") 

900 
proof 

901 
fix i 

902 
from A have Ai: "A i \<in> generated_ring" by auto 

903 
from generated_ringE[OF this] guess C . note C = this 

904 

905 
have "\<exists>F'. bij_betw F' {..<card C} C" 

906 
by (rule finite_same_card_bij[OF _ `finite C`]) auto 

907 
then guess F .. note F = this 

908 
def f \<equiv> "\<lambda>i. if i < card C then F i else {}" 

909 
then have f: "bij_betw f {..< card C} C" 

910 
by (intro bij_betw_cong[THEN iffD1, OF _ F]) auto 

911 
with C have "\<forall>j. f j \<in> M" 

912 
by (auto simp: Pi_iff f_def dest!: bij_betw_imp_funcset) 

913 
moreover 

914 
from f C have d_f: "disjoint_family_on f {..<card C}" 

915 
by (intro disjoint_image_disjoint_family_on) (auto simp: bij_betw_def) 

916 
then have "disjoint_family f" 

917 
by (auto simp: disjoint_family_on_def f_def) 

918 
moreover 

919 
have Ai_eq: "A i = (\<Union> x<card C. f x)" 

920 
using f C Ai unfolding bij_betw_def by (simp add: Union_image_eq[symmetric]) 

921 
then have "\<Union>range f = A i" 

922 
using f C Ai unfolding bij_betw_def by (auto simp: f_def) 

923 
moreover 

924 
{ have "(\<Sum>j. \<mu>_r (f j)) = (\<Sum>j. if j \<in> {..< card C} then \<mu>_r (f j) else 0)" 

925 
using volume_empty[OF V(1)] by (auto intro!: arg_cong[where f=suminf] simp: f_def) 

926 
also have "\<dots> = (\<Sum>j<card C. \<mu>_r (f j))" 

927 
by (rule sums_If_finite_set[THEN sums_unique, symmetric]) simp 

928 
also have "\<dots> = \<mu>_r (A i)" 

929 
using C f[THEN bij_betw_imp_funcset] unfolding Ai_eq 

930 
by (intro volume_finite_additive[OF V(1) _ d_f, symmetric]) 

931 
(auto simp: Pi_iff Ai_eq intro: generated_ringI_Basic) 

932 
finally have "\<mu>_r (A i) = (\<Sum>j. \<mu>_r (f j))" .. } 

933 
ultimately show "?P i" 

934 
by blast 

935 
qed 

936 
from choice[OF this] guess f .. note f = this 

937 
then have UN_f_eq: "(\<Union>i. split f (prod_decode i)) = (\<Union>i. A i)" 

938 
unfolding UN_extend_simps surj_prod_decode by (auto simp: set_eq_iff) 

939 

940 
have d: "disjoint_family (\<lambda>i. split f (prod_decode i))" 

941 
unfolding disjoint_family_on_def 

942 
proof (intro ballI impI) 

943 
fix m n :: nat assume "m \<noteq> n" 

944 
then have neq: "prod_decode m \<noteq> prod_decode n" 

945 
using inj_prod_decode[of UNIV] by (auto simp: inj_on_def) 

946 
show "split f (prod_decode m) \<inter> split f (prod_decode n) = {}" 

947 
proof cases 

948 
assume "fst (prod_decode m) = fst (prod_decode n)" 

949 
then show ?thesis 

950 
using neq f by (fastforce simp: disjoint_family_on_def) 

951 
next 

952 
assume neq: "fst (prod_decode m) \<noteq> fst (prod_decode n)" 

953 
have "split f (prod_decode m) \<subseteq> A (fst (prod_decode m))" 

954 
"split f (prod_decode n) \<subseteq> A (fst (prod_decode n))" 

955 
using f[THEN spec, of "fst (prod_decode m)"] 

956 
using f[THEN spec, of "fst (prod_decode n)"] 

957 
by (auto simp: set_eq_iff) 

958 
with f A neq show ?thesis 

959 
by (fastforce simp: disjoint_family_on_def subset_eq set_eq_iff) 

960 
qed 

961 
qed 

962 
from f have "(\<Sum>n. \<mu>_r (A n)) = (\<Sum>n. \<mu>_r (split f (prod_decode n)))" 

963 
by (intro suminf_ereal_2dimen[symmetric] positiveD2[OF pos] generated_ringI_Basic) 

964 
(auto split: prod.split) 

965 
also have "\<dots> = (\<Sum>n. \<mu> (split f (prod_decode n)))" 

966 
using f V(2) by (auto intro!: arg_cong[where f=suminf] split: prod.split) 

967 
also have "\<dots> = \<mu> (\<Union>i. split f (prod_decode i))" 

968 
using f `c \<in> C'` C' 

969 
by (intro ca[unfolded countably_additive_def, rule_format]) 

970 
(auto split: prod.split simp: UN_f_eq d UN_eq) 

971 
finally have "(\<Sum>n. \<mu>_r (A' n \<inter> c)) = \<mu> c" 

972 
using UN_f_eq UN_eq by (simp add: A_def) } 

973 
note eq = this 

974 

975 
have "(\<Sum>n. \<mu>_r (A' n)) = (\<Sum>n. \<Sum>c\<in>C'. \<mu>_r (A' n \<inter> c))" 

49394
52e636ace94e
removing find_theorems commands that were left in the developments accidently
bulwahn
parents:
47762
diff
changeset

976 
using C' A' 
47762  977 
by (subst volume_finite_additive[symmetric, OF V(1)]) 
978 
(auto simp: disjoint_def disjoint_family_on_def Union_image_eq[symmetric] simp del: Union_image_eq 

979 
intro!: G.Int G.finite_Union arg_cong[where f="\<lambda>X. suminf (\<lambda>i. \<mu>_r (X i))"] ext 

980 
intro: generated_ringI_Basic) 

981 
also have "\<dots> = (\<Sum>c\<in>C'. \<Sum>n. \<mu>_r (A' n \<inter> c))" 

982 
using C' A' 

983 
by (intro suminf_setsum_ereal positiveD2[OF pos] G.Int G.finite_Union) 

984 
(auto intro: generated_ringI_Basic) 

985 
also have "\<dots> = (\<Sum>c\<in>C'. \<mu>_r c)" 

986 
using eq V C' by (auto intro!: setsum_cong) 

987 
also have "\<dots> = \<mu>_r (\<Union>C')" 

988 
using C' Un_A 

989 
by (subst volume_finite_additive[symmetric, OF V(1)]) 

990 
(auto simp: disjoint_family_on_def disjoint_def Union_image_eq[symmetric] simp del: Union_image_eq 

991 
intro: generated_ringI_Basic) 

992 
finally show "(\<Sum>n. \<mu>_r (A' n)) = \<mu>_r (\<Union>i. A' i)" 

993 
using C' by simp 

994 
qed 

995 
from G.caratheodory'[OF `positive generated_ring \<mu>_r` `countably_additive generated_ring \<mu>_r`] 

996 
guess \<mu>' .. 

997 
with V show ?thesis 

998 
unfolding sigma_sets_generated_ring_eq 

999 
by (intro exI[of _ \<mu>']) (auto intro: generated_ringI_Basic) 

1000 
qed 

1001 

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

1002 
end 