author  hoelzl 
Tue, 22 Mar 2011 20:06:10 +0100  
changeset 42067  66c8281349ec 
parent 42066  6db76c88907a 
child 42145  8448713d48b7 
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 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

9 
imports Sigma_Algebra Extended_Real_Limits 
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 

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

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

17 
fixes f:: "nat \<times> nat \<Rightarrow> extreal" 
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 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

43 
by (auto intro!: SUPR_eq simp: setsum_cartesian_product reindex le_SUPI2 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

45 
SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg) 
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 
record 'a measure_space = "'a algebra" + 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

51 
measure :: "'a set \<Rightarrow> extreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

52 

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

53 
definition positive where "positive M f \<longleftrightarrow> f {} = (0::extreal) \<and> (\<forall>A\<in>sets M. 0 \<le> f A)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

54 

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

55 
definition additive where "additive 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

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

57 

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

58 
definition countably_additive :: "('a, 'b) algebra_scheme \<Rightarrow> ('a set \<Rightarrow> extreal) \<Rightarrow> bool" where 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

59 
"countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow> 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

61 

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

62 
definition increasing where "increasing 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

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

64 

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

65 
definition subadditive where "subadditive M f \<longleftrightarrow> 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

66 
(\<forall>x \<in> sets M. \<forall>y \<in> sets 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

67 

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

68 
definition countably_subadditive where "countably_subadditive 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

69 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow> 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

71 

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

72 
definition lambda_system where "lambda_system M f = {l \<in> sets M. 
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

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

74 

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

75 
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

76 
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

77 

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

78 
definition measure_set where "measure_set M f X = {r. 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

79 
\<exists>A. range A \<subseteq> sets 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

80 

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

81 
locale measure_space = sigma_algebra M for M :: "('a, 'b) measure_space_scheme" + 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

82 
assumes measure_positive: "positive M (measure 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

83 
and ca: "countably_additive M (measure M)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

84 

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

85 
abbreviation (in measure_space) "\<mu> \<equiv> measure M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

86 

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

87 
lemma (in measure_space) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

88 
shows empty_measure[simp, intro]: "\<mu> {} = 0" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

89 
and positive_measure[simp, intro!]: "\<And>A. A \<in> sets M \<Longrightarrow> 0 \<le> \<mu> A" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

91 

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

92 
lemma increasingD: 
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 
"increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

95 

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

96 
lemma subadditiveD: 
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 
"subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> sets M \<Longrightarrow> y \<in> sets M 
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 
\<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

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

100 

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

101 
lemma additiveD: 
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

102 
"additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> sets M \<Longrightarrow> y \<in> sets M 
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

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

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

105 

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 
lemma countably_additiveI: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

107 
assumes "\<And>A x. range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

109 
shows "countably_additive M f" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

110 
using assms by (simp add: countably_additive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

111 

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

113 

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

115 
assumes f: "f {} = 0" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

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

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

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

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

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

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

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

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

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

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

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

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

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

133 

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

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

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

136 
shows "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

137 
by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f] atLeast0LessThan) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

138 

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

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

140 
fixes f :: "'a set \<Rightarrow> 'b::{comm_monoid_add, t2_space}" 
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

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

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

143 

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

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

145 

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

146 
lemma (in algebra) lambda_system_eq: 
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

147 
shows "lambda_system M f = {l \<in> sets M. 
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

148 
\<forall>x \<in> sets 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

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

150 
have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M  l) \<inter> x = x  l" 
37032  151 
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

152 
show ?thesis 
37032  153 
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

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

155 

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

156 
lemma (in algebra) lambda_system_empty: 
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

157 
"positive M f \<Longrightarrow> {} \<in> lambda_system M f" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

158 
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

159 

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

160 
lemma 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

161 
"x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M" 
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

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

163 

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

164 
lemma (in algebra) lambda_system_Compl: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

165 
fixes f:: "'a set \<Rightarrow> extreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

167 
shows "space M  x \<in> lambda_system 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

168 
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

169 
have "x \<subseteq> space M" 
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 
by (metis sets_into_space lambda_system_sets x) 
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 
hence "space M  (space M  x) = x" 
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 
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

173 
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

174 
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

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

176 

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

177 
lemma (in algebra) lambda_system_Int: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

178 
fixes f:: "'a set \<Rightarrow> extreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

180 
shows "x \<inter> y \<in> lambda_system 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

181 
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

182 
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

183 
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

184 
fix 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

185 
assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M" 
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 
and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z  x) = f 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

187 
and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z  y) = f 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

188 
have "u  x \<inter> y \<in> sets M" 
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

189 
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

190 
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

191 
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

192 
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

193 
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

194 
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

195 
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

196 
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

197 
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

198 
= (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

199 
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

200 
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

201 
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

202 
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

203 
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

204 
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

205 
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

206 
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

207 
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

208 
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

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

210 

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

211 
lemma (in algebra) lambda_system_Un: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

212 
fixes f:: "'a set \<Rightarrow> extreal" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

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

216 
have "(space M  x) \<inter> (space M  y) \<in> sets M" 
38656  217 
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

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

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

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

221 
ultimately show ?thesis 
38656  222 
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

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

224 

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

225 
lemma (in algebra) lambda_system_algebra: 
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

226 
"positive M f \<Longrightarrow> algebra (M\<lparr>sets := lambda_system M f\<rparr>)" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

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

228 
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

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

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

232 
done 
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 algebra) lambda_system_strong_additive: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

237 
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

238 
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

239 
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

240 
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

241 
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

242 
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

243 
have "(z \<inter> (x \<union> y)) \<in> sets M" 
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

244 
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

245 
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

246 
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

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

248 

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

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

250 
"additive (M (sets := lambda_system 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

251 
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

252 
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

253 
assume disj: "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

254 
and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system 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

255 
hence "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_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

256 
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

257 
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

258 
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

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

260 

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

261 
lemma (in algebra) 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

262 
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

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

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

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

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

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

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

271 
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

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

274 
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

275 
by (simp add: range_binaryset_eq UN_binaryset_eq) 
38656  276 
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

277 
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

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

279 

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

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

281 
fixes A:: "nat \<Rightarrow> 'a set" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

282 
assumes f: "positive M f" and ad: "additive M f" and "finite S" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

283 
and A: "range A \<subseteq> sets M" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

284 
and disj: "disjoint_family_on A S" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

285 
shows "(\<Sum>i\<in>S. f (A i)) = f (\<Union>i\<in>S. A i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

286 
using `finite S` disj proof induct 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

287 
case empty 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

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

289 
case (insert s S) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

290 
then have "A s \<inter> (\<Union>i\<in>S. A i) = {}" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

291 
by (auto simp add: disjoint_family_on_def neq_iff) 
38656  292 
moreover 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

293 
have "A s \<in> sets M" using A by blast 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

294 
moreover have "(\<Union>i\<in>S. A i) \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

295 
using A `finite S` by auto 
38656  296 
moreover 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

297 
ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)" 
38656  298 
using ad UNION_in_sets A by (auto simp add: additive_def) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

299 
with insert show ?case using ad disjoint_family_on_mono[of S "insert s S" A] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

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

302 

38656  303 
lemma (in algebra) increasing_additive_bound: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

304 
fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> extreal" 
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

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

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

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

308 
and disj: "disjoint_family A" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

310 
proof (safe intro!: suminf_bound) 
38656  311 
fix N 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

312 
note disj_N = disjoint_family_on_mono[OF _ disj, of "{..<N}"] 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

313 
have "(\<Sum>i<N. f (A i)) = f (\<Union>i\<in>{..<N}. A i)" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

314 
by (rule additive_sum [OF f ad _ A]) (auto simp: disj_N) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

315 
also have "... \<le> f (space M)" using space_closed A 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

316 
by (intro increasingD[OF inc] finite_UN) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

317 
finally show "(\<Sum>i<N. f (A i)) \<le> f (space M)" by simp 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

318 
qed (insert f A, auto simp: positive_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

319 

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

320 
lemma lambda_system_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

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

323 

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

324 
lemma lambda_system_positive: 
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

325 
"positive M f \<Longrightarrow> positive (M (sets := lambda_system M f)) 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

326 
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

327 

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

328 
lemma (in algebra) lambda_system_strong_sum: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

329 
fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> extreal" 
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 
assumes f: "positive M f" and a: "a \<in> sets M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

333 
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

334 
proof (induct n) 
38656  335 
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

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

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

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

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

342 
interpret l: algebra "M\<lparr>sets := lambda_system M f\<rparr>" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

343 
using f by (rule lambda_system_algebra) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

344 
have 4: "UNION {0..<n} A \<in> lambda_system M f" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

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

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

347 
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

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

349 

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

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

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

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

353 
and disj: "disjoint_family A" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

354 
shows "(\<Union>i. A i) \<in> lambda_system 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

355 
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

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

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

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

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

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

363 
interpret ls: algebra "M\<lparr>sets := lambda_system M f\<rparr>" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

364 
using pos by (rule lambda_system_algebra) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

366 
by (metis A image_subset_iff lambda_system_sets) 
38656  367 

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

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

370 
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

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

372 
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

373 
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

374 
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

375 
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

376 
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

377 
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

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

379 
by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] allI 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

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

381 
{ 
38656  382 
fix a 
383 
assume a [iff]: "a \<in> sets M" 

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

384 
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

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

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

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

38656  390 
moreover 
33536  391 
have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj 
38656  392 
by (auto simp add: disjoint_family_on_def) 
393 
moreover 

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

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

397 
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

398 
using csa[unfolded countably_subadditive_def, rule_format, of "(\<lambda>i. a \<inter> A i)"] 
38656  399 
by (simp add: o_def) 
400 
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

401 
(\<Sum>i. f (a \<inter> A i)) + f (a  (\<Union>i. A i))" 
38656  402 
by (rule add_right_mono) 
403 
moreover 

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

404 
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

405 
proof (intro suminf_bound_add allI) 
33536  406 
fix n 
407 
have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" 

38656  408 
by (metis A'' UNION_in_sets) 
33536  409 
have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' 
37032  410 
by (blast intro: increasingD [OF inc] A'' UNION_in_sets) 
33536  411 
have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f" 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

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

418 
thus "(\<Sum>i<n. f (a \<inter> A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
38656  419 
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

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

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

422 
then show "\<And>i. 0 \<le> f (a \<inter> 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

423 
have "\<And>i. a  (\<Union>i. A i) \<in> sets M" using A'' by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

424 
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

425 
then show "f (a  (\<Union>i. A i)) \<noteq> \<infinity>" by auto 
33536  426 
qed 
38656  427 
ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
428 
by (rule order_trans) 

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

429 
next 
38656  430 
have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a  (\<Union>i. A i)))" 
37032  431 
by (blast intro: increasingD [OF inc] U_in) 
33536  432 
also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i))" 
37032  433 
by (blast intro: subadditiveD [OF sa] U_in) 
33536  434 
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

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

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

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

438 
thus ?thesis 
38656  439 
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

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

441 

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

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

443 
assumes oms: "outer_measure_space 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

444 
shows "measure_space \<lparr> space = space M, sets = lambda_system M f, measure = f \<rparr>" 
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

445 
(is "measure_space ?M") 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

446 
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

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

448 
by (metis oms outer_measure_space_def) 
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

449 
have alg: "algebra ?M" 
38656  450 
using lambda_system_algebra [of f, OF pos] 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

451 
by (simp add: algebra_iff_Un) 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41981
diff
changeset

452 
then 
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

453 
have "sigma_algebra ?M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

454 
using lambda_system_caratheodory [OF oms] 
38656  455 
by (simp add: sigma_algebra_disjoint_iff) 
456 
moreover 

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

457 
have "measure_space_axioms ?M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

458 
using pos lambda_system_caratheodory [OF oms] 
38656  459 
by (simp add: measure_space_axioms_def positive_def lambda_system_sets 
460 
countably_additive_def o_def) 

461 
ultimately 

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

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

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

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

465 

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

466 
lemma (in ring_of_sets) additive_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

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

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

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

471 
assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

472 
then have "y  x \<in> sets M" by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

474 
then have "f x + 0 \<le> f x + f (yx)" by (intro add_left_mono) auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

477 
also have "... = f y" 
37032  478 
by (metis Un_Diff_cancel Un_absorb1 xy(3)) 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

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

481 

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

482 
lemma (in ring_of_sets) countably_additive_additive: 
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

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

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

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

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

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

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

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

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

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

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

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

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

498 
thus "f (x \<union> y) = f x + f y" using posf x y 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

499 
by (auto simp add: Un suminf_binaryset_eq positive_def) 
38656  500 
qed 
501 

39096  502 
lemma inf_measure_nonempty: 
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

503 
assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b" "{} \<in> sets M" 
39096  504 
shows "f b \<in> measure_set M f a" 
505 
proof  

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

506 
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

507 
have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

508 
by (rule suminf_finite) (simp add: f[unfolded positive_def]) 
39096  509 
also have "... = f b" 
510 
by simp 

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

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

512 
by (auto intro!: exI [of _ ?A] 
39096  513 
simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) 
514 
qed 

515 

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

516 
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

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

519 
shows "Inf (measure_set M f s) = f s" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

520 
unfolding Inf_extreal_def 
38656  521 
proof (safe intro!: Greatest_equality) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

525 
A: "range A \<subseteq> sets 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

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

528 
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

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

530 
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

531 
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

532 
proof (rule ca[unfolded countably_additive_def, rule_format]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

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

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

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

540 
hence "f s = (\<Sum>i. f (A i \<inter> s))" 
37032  541 
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

542 
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

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

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

546 
fix N have "A N \<inter> s \<in> sets M" using A s by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

547 
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

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

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

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

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

554 
thus "y \<le> f s" 
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

555 
by (blast intro: inf_measure_nonempty [of _ f, OF posf s subset_refl]) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

557 

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

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

559 
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

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

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

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

563 
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

564 
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

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

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

567 

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

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

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

570 
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

571 
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

572 
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

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

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

575 

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

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

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

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

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

580 
show "Inf (measure_set M f {}) \<le> 0" 
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

581 
by (metis complete_lattice_class.Inf_lower `{} \<in> sets M` 
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

582 
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

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

584 

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

585 
lemma (in ring_of_sets) inf_measure_positive: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

586 
assumes p: "positive M f" and "{} \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

587 
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

588 
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

589 
show "Inf (measure_set M f {}) = 0" using inf_measure_empty[OF assms] by auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

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

592 

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

593 
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

594 
assumes posf: "positive 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

595 
shows "increasing \<lparr> space = space M, sets = Pow (space M) \<rparr> 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

596 
(\<lambda>x. Inf (measure_set M f x))" 
38656  597 
apply (auto simp add: increasing_def) 
598 
apply (rule complete_lattice_class.Inf_greatest) 

599 
apply (rule complete_lattice_class.Inf_lower) 

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

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

602 

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

603 
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

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

605 
and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets 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

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

607 
proof  
38656  608 
obtain A where A: "range A \<subseteq> sets 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

609 
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

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

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

612 
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

613 
have "\<forall>n. f (disjointed A n) \<le> f (A n)" 
38656  614 
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

615 
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

616 
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

617 
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

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

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

621 
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

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

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

626 
show ?thesis 
38656  627 
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

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

629 

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

630 
lemma (in ring_of_sets) inf_measure_close: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

631 
fixes e :: extreal 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

632 
assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" and "Inf (measure_set M f s) \<noteq> \<infinity>" 
38656  633 
shows "\<exists>A. range A \<subseteq> sets 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

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

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

636 
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

637 
using inf_measure_pos[OF posf, of s] by auto 
38656  638 
obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e" 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

639 
using Inf_extreal_close[OF fin e] by auto 
38656  640 
thus ?thesis 
641 
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

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

643 

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

644 
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

645 
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

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

647 
(\<lambda>x. Inf (measure_set M f x))" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

649 
fix A :: "nat \<Rightarrow> 'a set" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

650 
let "?outer B" = "Inf (measure_set M f B)" 
38656  651 
assume A: "range A \<subseteq> Pow (space M)" 
652 
and disj: "disjoint_family A" 

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

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

654 

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

655 
{ fix e :: extreal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

656 
hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and> 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

657 
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

658 
apply (safe intro!: choice inf_measure_close [of f, OF posf]) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

659 
using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

660 
then obtain BB 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

661 
where BB: "\<And>n. (range (BB n) \<subseteq> sets M)" 
38656  662 
and disjBB: "\<And>n. disjoint_family (BB n)" 
663 
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

664 
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

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

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

668 
have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

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

670 
by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal) 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

671 
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

672 
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

673 
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

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

675 
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

676 
using sum_eq_1 inf_measure_pos[OF posf] e 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41689
diff
changeset

677 
by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff) 
38656  678 
finally show ?thesis . 
679 
qed 

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

680 
def C \<equiv> "(split BB) o prod_decode" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

681 
have C: "!!n. C n \<in> sets M" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

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

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

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

686 
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" 
38656  687 
proof (auto simp add: C_def) 
688 
fix x i 

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

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

691 
by blast 

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

693 
by (metis prod_encode_inverse prod.cases) 

694 
qed 

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

695 
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

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

697 
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

698 
using BB posf[unfolded positive_def] 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

699 
by (force intro!: suminf_extreal_2dimen simp: o_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

700 
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

701 
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

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

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

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

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

706 
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

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

708 
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

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

710 

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

711 
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

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

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

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

715 
by (intro extreal_le_epsilon) auto 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

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

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

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

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

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

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

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

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

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

726 

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

727 
lemma (in ring_of_sets) inf_measure_outer: 
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

728 
"\<lbrakk> positive M f ; increasing M f \<rbrakk> 
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

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

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

731 
using inf_measure_pos[of M f] 
38656  732 
by (simp add: outer_measure_space_def inf_measure_empty 
733 
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

734 

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

735 
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

736 
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

737 
and add: "additive M f" 
42066
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

739 
(\<lambda>x. Inf (measure_set M f x))" 
38656  740 
proof (auto dest: sets_into_space 
741 
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

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

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

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

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

747 
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

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

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

750 
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

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

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

753 
then have "measure_set M f s \<noteq> {}" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

754 
by (auto simp: top_extreal_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

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

757 
fix r assume "r \<in> measure_set M f s" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

758 
then obtain A where A: "disjoint_family A" "range A \<subseteq> sets M" "s \<subseteq> (\<Union>i. A i)" 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

759 
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

760 
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

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

762 
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

763 
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

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

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

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

767 
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

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

769 
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

770 
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

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

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

773 
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

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

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

776 
using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def) 
6db76c88907a
generalized Caratheodory from algebra to ring_of_sets
hoelzl
parents:
42065
diff
changeset

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

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

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

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

781 
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

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

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

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

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

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

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

789 
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

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

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

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

794 
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

795 
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

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

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

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

800 
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

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

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

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

804 

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

805 
lemma measure_down: 
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

806 
"measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow> measure N = measure M \<Longrightarrow> measure_space M" 
38656  807 
by (simp add: measure_space_def measure_space_axioms_def positive_def 
808 
countably_additive_def) 

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

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

810 

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

811 
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

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

813 
shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> 
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

814 
measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>" 
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

815 
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

816 
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

817 
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

818 
let ?infm = "(\<lambda>x. Inf (measure_set M f x))" 
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

819 
def ls \<equiv> "lambda_system (space = space M, sets = Pow (space M)) ?infm" 
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

820 
have mls: "measure_space \<lparr>space = space M, sets = ls, measure = ?infm\<rparr>" 
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

821 
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

822 
[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

823 
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

824 
hence sls: "sigma_algebra (space = space M, sets = ls, measure = ?infm)" 
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

825 
by (simp add: measure_space_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

826 
have "sets M \<subseteq> ls" 
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

827 
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

828 
(metis ca posf inc countably_additive_additive algebra_subset_lambda_system) 
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

829 
hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" 
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

830 
using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] 
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

831 
by simp 
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

832 
have "measure_space \<lparr> space = space M, sets = sets (sigma M), measure = ?infm \<rparr>" 
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

833 
unfolding sigma_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

834 
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

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

836 
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

837 
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

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

839 

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

840 
end 