author  hoelzl 
Tue, 22 Mar 2011 18:53:05 +0100  
changeset 42066  6db76c88907a 
parent 42065  2b98b4c2e2f1 
child 42067  66c8281349ec 
permissions  rwrr 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

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

2 

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

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

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

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

6 

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

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

8 
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

9 
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

10 
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

11 
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

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

13 
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

14 
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

15 
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

16 
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

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

18 
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

19 
{ 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

20 
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

21 
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

22 
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

23 
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

24 
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

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

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

27 
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

28 
{ 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

29 
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

30 
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

31 
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

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

33 
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

34 
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

35 
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

36 
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

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

38 

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

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

40 

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

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

42 

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

43 
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

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

45 

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

46 
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

47 

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

48 
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

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

50 

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

51 
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

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

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

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

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

57 

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

58 
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

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

60 

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

61 
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

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

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

64 

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

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

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

69 
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

70 

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

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

73 

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

74 
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

75 
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

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

77 

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

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

79 

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

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

81 
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

82 
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

83 
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

84 

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

85 
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

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

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

88 

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

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

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

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

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

93 

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

94 
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

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

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

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

98 

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

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

100 
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

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

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

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

104 

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

106 

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

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

109 
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

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

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

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

114 
show "(\<Sum>i < Suc (Suc n). f (binaryset A B i)) = f A + f B" 
35582  115 
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

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

117 
moreover 
35582  118 
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

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

120 
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

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

122 
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

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

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

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

126 

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

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

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

129 
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

130 
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

131 

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

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

133 
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

134 
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

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

136 

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

137 
subsection {* Lambda Systems *} 
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 (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

140 
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

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

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

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

145 
show ?thesis 
37032  146 
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

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

148 

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

149 
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

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

151 
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

152 

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

153 
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

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

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

156 

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

157 
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

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

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

160 
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

161 
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

162 
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

163 
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

164 
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

165 
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

166 
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

167 
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

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

169 

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

170 
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

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

172 
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

173 
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

174 
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

175 
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

176 
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

177 
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

178 
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

179 
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

180 
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

181 
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

182 
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

183 
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

184 
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

185 
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

186 
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

187 
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

188 
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

189 
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

190 
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

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

192 
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

193 
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

194 
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

195 
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

196 
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

197 
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

198 
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

199 
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

200 
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

201 
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

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

203 

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

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

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

206 
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

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

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

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

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

212 
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

213 
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

214 
ultimately show ?thesis 
38656  215 
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

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

217 

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

218 
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

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

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

221 
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

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

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

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

226 

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

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

228 
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

229 
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

230 
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

231 
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

232 
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

233 
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

234 
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

235 
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

236 
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

237 
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

238 
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

239 
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

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

241 

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

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

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

244 
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

245 
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

246 
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

247 
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

248 
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

249 
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

250 
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

251 
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

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

253 

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

254 
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

255 
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

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

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

259 
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

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

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

264 
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

265 
using cs by (auto simp add: countably_subadditive_def) 
35582  266 
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

267 
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

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

270 
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

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

272 

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

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

274 
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

275 
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

276 
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

277 
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

278 
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

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

280 
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

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

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

283 
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

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

286 
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

287 
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

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

290 
ultimately have "f (A s \<union> (\<Union>i\<in>S. A i)) = f (A s) + f(\<Union>i\<in>S. A i)" 
38656  291 
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

292 
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

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

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

295 

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

297 
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

298 
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

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

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

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

302 
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

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

305 
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

306 
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

307 
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

308 
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

309 
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

310 
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

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

312 

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

313 
lemma lambda_system_increasing: 
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

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

316 

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

317 
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

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

319 
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

320 

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

321 
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

322 
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

323 
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

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

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

326 
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

327 
proof (induct n) 
38656  328 
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

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

331 
have 2: "A n \<inter> UNION {0..<n} A = {}" using disj 
38656  332 
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

333 
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

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

335 
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

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

337 
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

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

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

340 
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

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

342 

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

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

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

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

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

347 
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

348 
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

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

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

352 
have sa: "subadditive M f" 
38656  353 
by (metis countably_subadditive_subadditive csa pos) 
354 
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

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

356 
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

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

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

359 
by (metis A image_subset_iff lambda_system_sets) 
38656  360 

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

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

363 
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

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

365 
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

366 
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

367 
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

368 
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

369 
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

370 
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

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

372 
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

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

374 
{ 
38656  375 
fix a 
376 
assume a [iff]: "a \<in> sets M" 

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

377 
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

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

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

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

38656  383 
moreover 
33536  384 
have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj 
38656  385 
by (auto simp add: disjoint_family_on_def) 
386 
moreover 

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

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

390 
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

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

394 
(\<Sum>i. f (a \<inter> A i)) + f (a  (\<Union>i. A i))" 
38656  395 
by (rule add_right_mono) 
396 
moreover 

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

397 
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

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

38656  401 
by (metis A'' UNION_in_sets) 
33536  402 
have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' 
37032  403 
by (blast intro: increasingD [OF inc] A'' UNION_in_sets) 
33536  404 
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

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

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

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

414 
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

415 
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

416 
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

417 
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

418 
then show "f (a  (\<Union>i. A i)) \<noteq> \<infinity>" by auto 
33536  419 
qed 
38656  420 
ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i)) \<le> f a" 
421 
by (rule order_trans) 

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

422 
next 
38656  423 
have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a  (\<Union>i. A i)))" 
37032  424 
by (blast intro: increasingD [OF inc] U_in) 
33536  425 
also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a  (\<Union>i. A i))" 
37032  426 
by (blast intro: subadditiveD [OF sa] U_in) 
33536  427 
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

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

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

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

431 
thus ?thesis 
38656  432 
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

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

434 

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

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

436 
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

437 
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

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

439 
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

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

441 
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

442 
have alg: "algebra ?M" 
38656  443 
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

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

445 
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

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

447 
using lambda_system_caratheodory [OF oms] 
38656  448 
by (simp add: sigma_algebra_disjoint_iff) 
449 
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

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

451 
using pos lambda_system_caratheodory [OF oms] 
38656  452 
by (simp add: measure_space_axioms_def positive_def lambda_system_sets 
453 
countably_additive_def o_def) 

454 
ultimately 

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

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

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

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

458 

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

459 
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

460 
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

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

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

464 
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

465 
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

466 
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

467 
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

468 
also have "... = f (x \<union> (yx))" using addf 
37032  469 
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

470 
also have "... = f y" 
37032  471 
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

472 
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

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

474 

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

475 
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

476 
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

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

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

480 
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

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

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

485 
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

486 
using ca 
38656  487 
by (simp add: countably_additive_def) 
488 
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

489 
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

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

491 
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

492 
by (auto simp add: Un suminf_binaryset_eq positive_def) 
38656  493 
qed 
494 

39096  495 
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

496 
assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b" "{} \<in> sets M" 
39096  497 
shows "f b \<in> measure_set M f a" 
498 
proof  

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

499 
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

500 
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

501 
by (rule suminf_finite) (simp add: f[unfolded positive_def]) 
39096  502 
also have "... = f b" 
503 
by simp 

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

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

505 
by (auto intro!: exI [of _ ?A] 
39096  506 
simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def) 
507 
qed 

508 

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

509 
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

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

512 
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

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

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

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

518 
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

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

521 
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

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

523 
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

524 
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

525 
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

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

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

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

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

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

535 
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

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

537 
fix n show "f (A n \<inter> s) \<le> f (A n)" using A s 
38656  538 
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

539 
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

540 
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

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

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

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

545 
fix y 
38656  546 
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

547 
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

548 
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

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

550 

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

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

552 
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

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

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

555 
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

556 
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

557 
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

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

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

560 

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

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

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

563 
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

564 
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

565 
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

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

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

568 

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

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

570 
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

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

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

573 
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

574 
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

575 
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

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

577 

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

578 
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

579 
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

580 
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

581 
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

582 
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

583 
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

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

585 

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

586 
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

587 
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

588 
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

589 
(\<lambda>x. Inf (measure_set M f x))" 
38656  590 
apply (auto simp add: increasing_def) 
591 
apply (rule complete_lattice_class.Inf_greatest) 

592 
apply (rule complete_lattice_class.Inf_lower) 

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

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

595 

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

596 
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

597 
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

598 
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

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

600 
proof  
38656  601 
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

602 
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

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

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

605 
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

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

608 
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

609 
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

610 
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

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

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

614 
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

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

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

619 
show ?thesis 
38656  620 
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

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

622 

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

623 
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

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

625 
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  626 
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

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

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

629 
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

630 
using inf_measure_pos[OF posf, of s] by auto 
38656  631 
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

632 
using Inf_extreal_close[OF fin e] by auto 
38656  633 
thus ?thesis 
634 
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

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

636 

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

637 
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

638 
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

639 
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

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

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

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

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

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

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

647 

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

648 
{ 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

649 
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

650 
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

651 
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

652 
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

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

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

657 
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

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

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

661 
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

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

663 
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

664 
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

665 
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

666 
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

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

668 
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

669 
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

670 
by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff) 
38656  671 
finally show ?thesis . 
672 
qed 

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

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

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

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

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

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

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

679 
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" 
38656  680 
proof (auto simp add: C_def) 
681 
fix x i 

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

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

684 
by blast 

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

686 
by (metis prod_encode_inverse prod.cases) 

687 
qed 

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

688 
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

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

690 
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

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

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

693 
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

694 
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

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

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

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

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

699 
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

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

701 
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

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

703 

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

704 
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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

719 

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

720 
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

721 
"\<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

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

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

724 
using inf_measure_pos[of M f] 
38656  725 
by (simp add: outer_measure_space_def inf_measure_empty 
726 
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

727 

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

728 
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

729 
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

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

731 
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

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

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

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

737 
and s: "s \<subseteq> space M" 
38656  738 
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

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

740 
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

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

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

743 
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

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

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

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

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

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

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

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

751 
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

752 
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

753 
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

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

755 
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

756 
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

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

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

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

760 
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

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

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

768 
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

769 
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

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

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

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

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

774 
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

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

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

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

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

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

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

782 
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

783 
by (metis Un_Diff_Int Un_commute) 
38656  784 
also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (sx))" 
785 
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

786 
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

787 
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

788 
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

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

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

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

793 
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

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

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

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

797 

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

798 
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

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

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

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

803 

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

804 
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

805 
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

806 
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

807 
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

808 
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

809 
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

810 
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

811 
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

812 
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

813 
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

814 
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

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

816 
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

817 
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

818 
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

819 
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

820 
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

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

822 
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

823 
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

824 
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

825 
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

826 
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

827 
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

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

829 
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

830 
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

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

832 

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

833 
end 