author | huffman |
Wed, 10 Mar 2010 15:57:01 -0800 | |
changeset 35704 | 5007843dae33 |
parent 35582 | b16d99a72dc9 |
child 36649 | bfd8c550faa6 |
permissions | -rw-r--r-- |
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 |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
4 |
imports Sigma_Algebra SupInf SeriesPlus |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
5 |
begin |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
6 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
7 |
text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
8 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
9 |
subsection {* Measure Spaces *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
10 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
11 |
text {*A measure assigns a nonnegative real to every measurable set. |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
12 |
It is countably additive for disjoint sets.*} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
13 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
14 |
record 'a measure_space = "'a algebra" + |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
15 |
measure:: "'a set \<Rightarrow> real" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
16 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
17 |
definition |
35582 | 18 |
disjoint_family_on where |
19 |
"disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" |
|
20 |
||
21 |
abbreviation |
|
22 |
"disjoint_family A \<equiv> disjoint_family_on A UNIV" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
23 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
24 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
25 |
positive where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
26 |
"positive M f \<longleftrightarrow> f {} = (0::real) & (\<forall>x \<in> sets M. 0 \<le> f x)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
27 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
28 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
29 |
additive where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
30 |
"additive M f \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
31 |
(\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
32 |
\<longrightarrow> f (x \<union> y) = f x + f y)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
33 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
34 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
35 |
countably_additive where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
36 |
"countably_additive M f \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
37 |
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
38 |
disjoint_family A \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
39 |
(\<Union>i. A i) \<in> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
40 |
(\<lambda>n. f (A n)) sums f (\<Union>i. A i))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
41 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
42 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
43 |
increasing where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
44 |
"increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
45 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
46 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
47 |
subadditive where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
48 |
"subadditive M f \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
49 |
(\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
50 |
\<longrightarrow> f (x \<union> y) \<le> f x + f y)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
51 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
52 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
53 |
countably_subadditive where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
54 |
"countably_subadditive M f \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
55 |
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
56 |
disjoint_family A \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
57 |
(\<Union>i. A i) \<in> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
58 |
summable (f o A) \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
59 |
f (\<Union>i. A i) \<le> suminf (\<lambda>n. f (A n)))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
60 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
61 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
62 |
lambda_system where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
63 |
"lambda_system M f = |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
64 |
{l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
65 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
66 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
67 |
outer_measure_space where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
68 |
"outer_measure_space M f \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
69 |
positive M f & increasing M f & countably_subadditive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
70 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
71 |
definition |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
72 |
measure_set where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
73 |
"measure_set M f X = |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
74 |
{r . \<exists>A. range A \<subseteq> sets M & disjoint_family A & X \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
75 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
76 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
77 |
locale measure_space = sigma_algebra + |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
78 |
assumes positive: "!!a. a \<in> sets M \<Longrightarrow> 0 \<le> measure M a" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
79 |
and empty_measure [simp]: "measure M {} = (0::real)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
80 |
and ca: "countably_additive M (measure M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
81 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
82 |
subsection {* Basic Lemmas *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
83 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
84 |
lemma positive_imp_0: "positive M f \<Longrightarrow> f {} = 0" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
85 |
by (simp add: positive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
86 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
87 |
lemma positive_imp_pos: "positive M f \<Longrightarrow> x \<in> sets M \<Longrightarrow> 0 \<le> f x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
88 |
by (simp add: positive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
89 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
90 |
lemma increasingD: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
91 |
"increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
92 |
by (auto simp add: increasing_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 subadditiveD: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
95 |
"subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
96 |
\<Longrightarrow> f (x \<union> y) \<le> f x + f y" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
97 |
by (auto simp add: subadditive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
98 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
99 |
lemma additiveD: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
100 |
"additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
101 |
\<Longrightarrow> f (x \<union> y) = f x + f y" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
102 |
by (auto simp add: additive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
103 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
104 |
lemma countably_additiveD: |
35582 | 105 |
"countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
106 |
\<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n)) sums f (\<Union>i. A i)" |
35582 | 107 |
by (simp add: countably_additive_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
108 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
109 |
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
110 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
111 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
112 |
lemma Int_Diff_Un: "A \<inter> B \<union> (A - B) = A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
113 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
114 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
115 |
lemma disjoint_family_subset: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
116 |
"disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B" |
35582 | 117 |
by (force simp add: disjoint_family_on_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
118 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
119 |
subsection {* A Two-Element Series *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
120 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
121 |
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set " |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
122 |
where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
123 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
124 |
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" |
35582 | 125 |
apply (simp add: binaryset_def) |
126 |
apply (rule set_ext) |
|
127 |
apply (auto simp add: image_iff) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
128 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
129 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
130 |
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B" |
35582 | 131 |
by (simp add: UNION_eq_Union_image range_binaryset_eq) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
132 |
|
35582 | 133 |
lemma LIMSEQ_binaryset: |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
134 |
assumes f: "f {} = 0" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
135 |
shows "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
136 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
137 |
have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)" |
35582 | 138 |
proof |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
139 |
fix n |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
140 |
show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B" |
35582 | 141 |
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
|
142 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
143 |
moreover |
35582 | 144 |
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
|
145 |
ultimately |
35582 | 146 |
have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
147 |
by metis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
148 |
hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
149 |
by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
150 |
thus ?thesis by (rule LIMSEQ_offset [where k=2]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
151 |
qed |
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 binaryset_sums: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
154 |
assumes f: "f {} = 0" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
155 |
shows "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
156 |
by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
157 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
158 |
lemma suminf_binaryset_eq: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
159 |
"f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
160 |
by (metis binaryset_sums sums_unique) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
161 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
162 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
163 |
subsection {* Lambda Systems *} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
164 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
165 |
lemma (in algebra) lambda_system_eq: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
166 |
"lambda_system M f = |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
167 |
{l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
168 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
169 |
have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
170 |
by (metis Diff_eq Int_Diff Int_absorb1 Int_commute sets_into_space) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
171 |
show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
172 |
by (auto simp add: lambda_system_def) (metis Diff_Compl Int_commute)+ |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
173 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
174 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
175 |
lemma (in algebra) lambda_system_empty: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
176 |
"positive M f \<Longrightarrow> {} \<in> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
177 |
by (auto simp add: positive_def lambda_system_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
178 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
179 |
lemma lambda_system_sets: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
180 |
"x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
181 |
by (simp add: lambda_system_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
182 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
183 |
lemma (in algebra) lambda_system_Compl: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
184 |
fixes f:: "'a set \<Rightarrow> real" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
185 |
assumes x: "x \<in> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
186 |
shows "space M - x \<in> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
187 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
188 |
have "x \<subseteq> space M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
189 |
by (metis sets_into_space lambda_system_sets x) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
190 |
hence "space M - (space M - x) = x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
191 |
by (metis double_diff equalityE) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
192 |
with x show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
193 |
by (force simp add: lambda_system_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
194 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
195 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
196 |
lemma (in algebra) lambda_system_Int: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
197 |
fixes f:: "'a set \<Rightarrow> real" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
198 |
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
|
199 |
shows "x \<inter> y \<in> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
200 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
201 |
from xl yl show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
202 |
proof (auto simp add: positive_def lambda_system_eq Int) |
33536 | 203 |
fix u |
204 |
assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
205 |
and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
206 |
and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z" |
33536 | 207 |
have "u - x \<inter> y \<in> sets M" |
208 |
by (metis Diff Diff_Int Un u x y) |
|
209 |
moreover |
|
210 |
have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast |
|
211 |
moreover |
|
212 |
have "u - x \<inter> y - y = u - y" by blast |
|
213 |
ultimately |
|
214 |
have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy |
|
215 |
by force |
|
216 |
have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
217 |
= (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)" |
33536 | 218 |
by (simp add: ey) |
219 |
also have "... = (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)" |
|
220 |
by (simp add: Int_ac) |
|
221 |
also have "... = f (u \<inter> y) + f (u - y)" |
|
222 |
using fx [THEN bspec, of "u \<inter> y"] Int y u |
|
223 |
by force |
|
224 |
also have "... = f u" |
|
225 |
by (metis fy u) |
|
226 |
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
|
227 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
228 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
229 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
230 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
231 |
lemma (in algebra) lambda_system_Un: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
232 |
fixes f:: "'a set \<Rightarrow> real" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
233 |
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
|
234 |
shows "x \<union> y \<in> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
235 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
236 |
have "(space M - x) \<inter> (space M - y) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
237 |
by (metis Diff_Un Un compl_sets lambda_system_sets xl yl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
238 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
239 |
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
|
240 |
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
|
241 |
ultimately show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
242 |
by (metis lambda_system_Compl lambda_system_Int xl yl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
243 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
244 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
245 |
lemma (in algebra) lambda_system_algebra: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
246 |
"positive M f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
247 |
apply (auto simp add: algebra_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
248 |
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
|
249 |
apply (metis lambda_system_empty) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
250 |
apply (metis lambda_system_Compl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
251 |
apply (metis lambda_system_Un) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
252 |
done |
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) lambda_system_strong_additive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
255 |
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
|
256 |
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
|
257 |
shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
258 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
259 |
have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
260 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
261 |
have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
262 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
263 |
have "(z \<inter> (x \<union> y)) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
264 |
by (metis Int Un lambda_system_sets xl yl z) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
265 |
ultimately show ?thesis using xl yl |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
266 |
by (simp add: lambda_system_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
267 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
268 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
269 |
lemma (in algebra) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
270 |
by (metis Int_absorb1 sets_into_space) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
271 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
272 |
lemma (in algebra) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
273 |
by (metis Int_absorb2 sets_into_space) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
274 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
275 |
lemma (in algebra) lambda_system_additive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
276 |
"additive (M (|sets := lambda_system M f|)) f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
277 |
proof (auto simp add: additive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
278 |
fix x and y |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
279 |
assume disj: "x \<inter> y = {}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
280 |
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
|
281 |
hence "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+ |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
282 |
thus "f (x \<union> y) = f x + f y" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
283 |
using lambda_system_strong_additive [OF top disj xl yl] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
284 |
by (simp add: Un) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
285 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
286 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
287 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
288 |
lemma (in algebra) countably_subadditive_subadditive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
289 |
assumes f: "positive M f" and cs: "countably_subadditive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
290 |
shows "subadditive M f" |
35582 | 291 |
proof (auto simp add: subadditive_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
292 |
fix x y |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
293 |
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
|
294 |
hence "disjoint_family (binaryset x y)" |
35582 | 295 |
by (auto simp add: disjoint_family_on_def binaryset_def) |
296 |
hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> |
|
297 |
(\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
298 |
summable (f o (binaryset x y)) \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
299 |
f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))" |
35582 | 300 |
using cs by (simp add: countably_subadditive_def) |
301 |
hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
302 |
summable (f o (binaryset x y)) \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
303 |
f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
304 |
by (simp add: range_binaryset_eq UN_binaryset_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
305 |
thus "f (x \<union> y) \<le> f x + f y" using f x y binaryset_sums |
35582 | 306 |
by (auto simp add: Un sums_iff positive_def o_def) |
307 |
qed |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
308 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
309 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
310 |
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set " |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
311 |
where "disjointed A n = A n - (\<Union>i\<in>{0..<n}. A i)" |
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 finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
314 |
proof (induct n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
315 |
case 0 show ?case by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
316 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
317 |
case (Suc n) |
35582 | 318 |
thus ?case by (simp add: atLeastLessThanSuc disjointed_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
319 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
320 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
321 |
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)" |
35582 | 322 |
apply (rule UN_finite2_eq [where k=0]) |
323 |
apply (simp add: finite_UN_disjointed_eq) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
324 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
325 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
326 |
lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
327 |
by (auto simp add: disjointed_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
328 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
329 |
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" |
35582 | 330 |
by (simp add: disjoint_family_on_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
331 |
(metis neq_iff Int_commute less_disjoint_disjointed) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
332 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
333 |
lemma disjointed_subset: "disjointed A n \<subseteq> A n" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
334 |
by (auto simp add: disjointed_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
335 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
336 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
337 |
lemma (in algebra) UNION_in_sets: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
338 |
fixes A:: "nat \<Rightarrow> 'a set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
339 |
assumes A: "range A \<subseteq> sets M " |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
340 |
shows "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
341 |
proof (induct n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
342 |
case 0 show ?case by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
343 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
344 |
case (Suc n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
345 |
thus ?case |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
346 |
by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
347 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
348 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
349 |
lemma (in algebra) range_disjointed_sets: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
350 |
assumes A: "range A \<subseteq> sets M " |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
351 |
shows "range (disjointed A) \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
352 |
proof (auto simp add: disjointed_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
353 |
fix n |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
354 |
show "A n - (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
355 |
by (metis A Diff UNIV_I disjointed_def image_subset_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
356 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
357 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
358 |
lemma sigma_algebra_disjoint_iff: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
359 |
"sigma_algebra M \<longleftrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
360 |
algebra M & |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
361 |
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
362 |
(\<Union>i::nat. A i) \<in> sets M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
363 |
proof (auto simp add: sigma_algebra_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
364 |
fix A :: "nat \<Rightarrow> 'a set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
365 |
assume M: "algebra M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
366 |
and A: "range A \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
367 |
and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
368 |
disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
369 |
hence "range (disjointed A) \<subseteq> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
370 |
disjoint_family (disjointed A) \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
371 |
(\<Union>i. disjointed A i) \<in> sets M" by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
372 |
hence "(\<Union>i. disjointed A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
373 |
by (simp add: algebra.range_disjointed_sets M A disjoint_family_disjointed) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
374 |
thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
375 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
376 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
377 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
378 |
lemma (in algebra) additive_sum: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
379 |
fixes A:: "nat \<Rightarrow> 'a set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
380 |
assumes f: "positive M f" and ad: "additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
381 |
and A: "range A \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
382 |
and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
383 |
shows "setsum (f o A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
384 |
proof (induct n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
385 |
case 0 show ?case using f by (simp add: positive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
386 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
387 |
case (Suc n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
388 |
have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj |
35582 | 389 |
by (auto simp add: disjoint_family_on_def neq_iff) blast |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
390 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
391 |
have "A n \<in> sets M" using A by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
392 |
moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
393 |
by (metis A UNION_in_sets atLeast0LessThan) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
394 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
395 |
ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
396 |
using ad UNION_in_sets A by (auto simp add: additive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
397 |
with Suc.hyps show ?case using ad |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
398 |
by (auto simp add: atLeastLessThanSuc additive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
399 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
400 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
401 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
402 |
lemma countably_subadditiveD: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
403 |
"countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
404 |
(\<Union>i. A i) \<in> sets M \<Longrightarrow> summable (f o A) \<Longrightarrow> f (\<Union>i. A i) \<le> suminf (f o A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
405 |
by (auto simp add: countably_subadditive_def o_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
406 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
407 |
lemma (in algebra) increasing_additive_summable: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
408 |
fixes A:: "nat \<Rightarrow> 'a set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
409 |
assumes f: "positive M f" and ad: "additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
410 |
and inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
411 |
and A: "range A \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
412 |
and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
413 |
shows "summable (f o A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
414 |
proof (rule pos_summable) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
415 |
fix n |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
416 |
show "0 \<le> (f \<circ> A) n" using f A |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
417 |
by (force simp add: positive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
418 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
419 |
fix n |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
420 |
have "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
421 |
by (rule additive_sum [OF f ad A disj]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
422 |
also have "... \<le> f (space M)" using space_closed A |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
423 |
by (blast intro: increasingD [OF inc] UNION_in_sets top) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
424 |
finally show "setsum (f \<circ> A) {0..<n} \<le> f (space M)" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
425 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
426 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
427 |
lemma lambda_system_positive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
428 |
"positive M f \<Longrightarrow> positive (M (|sets := lambda_system M f|)) f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
429 |
by (simp add: positive_def lambda_system_def) |
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 |
lemma lambda_system_increasing: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
432 |
"increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
433 |
by (simp add: increasing_def lambda_system_def) |
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 algebra) lambda_system_strong_sum: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
436 |
fixes A:: "nat \<Rightarrow> 'a set" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
437 |
assumes f: "positive M f" and a: "a \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
438 |
and A: "range A \<subseteq> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
439 |
and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
440 |
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
|
441 |
proof (induct n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
442 |
case 0 show ?case using f by (simp add: positive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
443 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
444 |
case (Suc n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
445 |
have 2: "A n \<inter> UNION {0..<n} A = {}" using disj |
35582 | 446 |
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
|
447 |
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
|
448 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
449 |
have 4: "UNION {0..<n} A \<in> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
450 |
using A algebra.UNION_in_sets [OF local.lambda_system_algebra [OF f]] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
451 |
by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
452 |
from Suc.hyps show ?case |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
453 |
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
|
454 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
455 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
456 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
457 |
lemma (in sigma_algebra) lambda_system_caratheodory: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
458 |
assumes oms: "outer_measure_space M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
459 |
and A: "range A \<subseteq> lambda_system M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
460 |
and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
461 |
shows "(\<Union>i. A i) \<in> lambda_system M f & (f \<circ> A) sums f (\<Union>i. A i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
462 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
463 |
have pos: "positive M f" and inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
464 |
and csa: "countably_subadditive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
465 |
by (metis oms outer_measure_space_def)+ |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
466 |
have sa: "subadditive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
467 |
by (metis countably_subadditive_subadditive csa pos) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
468 |
have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
469 |
by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
470 |
have alg_ls: "algebra (M(|sets := lambda_system M f|))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
471 |
by (rule lambda_system_algebra [OF pos]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
472 |
have A'': "range A \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
473 |
by (metis A image_subset_iff lambda_system_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
474 |
have sumfA: "summable (f \<circ> A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
475 |
by (metis algebra.increasing_additive_summable [OF alg_ls] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
476 |
lambda_system_positive lambda_system_additive lambda_system_increasing |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
477 |
A' oms outer_measure_space_def disj) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
478 |
have U_in: "(\<Union>i. A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
479 |
by (metis A countable_UN image_subset_iff lambda_system_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
480 |
have U_eq: "f (\<Union>i. A i) = suminf (f o A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
481 |
proof (rule antisym) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
482 |
show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)" |
33536 | 483 |
by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
484 |
show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)" |
33536 | 485 |
by (rule suminf_le [OF sumfA]) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
486 |
(metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right |
33536 | 487 |
lambda_system_positive lambda_system_additive |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
488 |
subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
489 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
490 |
{ |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
491 |
fix a |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
492 |
assume a [iff]: "a \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
493 |
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
|
494 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
495 |
have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' |
33536 | 496 |
apply - |
497 |
apply (rule summable_comparison_test [OF _ sumfA]) |
|
498 |
apply (rule_tac x="0" in exI) |
|
499 |
apply (simp add: positive_def) |
|
500 |
apply (auto simp add: ) |
|
501 |
apply (subst abs_of_nonneg) |
|
502 |
apply (metis A'' Int UNIV_I a image_subset_iff) |
|
503 |
apply (blast intro: increasingD [OF inc] a) |
|
504 |
done |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
505 |
show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
506 |
proof (rule antisym) |
33536 | 507 |
have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A'' |
508 |
by blast |
|
509 |
moreover |
|
510 |
have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj |
|
35582 | 511 |
by (auto simp add: disjoint_family_on_def) |
33536 | 512 |
moreover |
513 |
have "a \<inter> (\<Union>i. A i) \<in> sets M" |
|
514 |
by (metis Int U_in a) |
|
515 |
ultimately |
|
516 |
have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" |
|
517 |
using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ |
|
518 |
by (simp add: o_def) |
|
519 |
moreover |
|
520 |
have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) \<le> f a - f (a - (\<Union>i. A i))" |
|
521 |
proof (rule suminf_le [OF summ]) |
|
522 |
fix n |
|
523 |
have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" |
|
524 |
by (metis A'' UNION_in_sets) |
|
525 |
have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A'' |
|
526 |
by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) |
|
527 |
have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f" |
|
528 |
using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]] |
|
529 |
by (simp add: A) |
|
530 |
hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a" |
|
531 |
by (simp add: lambda_system_eq UNION_in Diff_Compl a) |
|
532 |
have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))" |
|
533 |
by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
534 |
UNION_in U_in a) |
33536 | 535 |
thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))" |
536 |
using eq_fa |
|
537 |
by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
538 |
a A disj) |
33536 | 539 |
qed |
540 |
ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" |
|
541 |
by arith |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
542 |
next |
33536 | 543 |
have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" |
544 |
by (blast intro: increasingD [OF inc] a U_in) |
|
545 |
also have "... \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" |
|
546 |
by (blast intro: subadditiveD [OF sa] Int Diff U_in) |
|
547 |
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
|
548 |
qed |
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 |
} |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
551 |
thus ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
552 |
by (simp add: lambda_system_eq sums_iff U_eq U_in sumfA) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
553 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
554 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
555 |
lemma (in sigma_algebra) caratheodory_lemma: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
556 |
assumes oms: "outer_measure_space M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
557 |
shows "measure_space (|space = space M, sets = lambda_system M f, measure = f|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
558 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
559 |
have pos: "positive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
560 |
by (metis oms outer_measure_space_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
561 |
have alg: "algebra (|space = space M, sets = lambda_system M f, measure = f|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
562 |
using lambda_system_algebra [OF pos] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
563 |
by (simp add: algebra_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
564 |
then moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
565 |
have "sigma_algebra (|space = space M, sets = lambda_system M f, measure = f|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
566 |
using lambda_system_caratheodory [OF oms] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
567 |
by (simp add: sigma_algebra_disjoint_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
568 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
569 |
have "measure_space_axioms (|space = space M, sets = lambda_system M f, measure = f|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
570 |
using pos lambda_system_caratheodory [OF oms] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
571 |
by (simp add: measure_space_axioms_def positive_def lambda_system_sets |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
572 |
countably_additive_def o_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
573 |
ultimately |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
574 |
show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
575 |
by intro_locales (auto simp add: sigma_algebra_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
576 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
577 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
578 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
579 |
lemma (in algebra) inf_measure_nonempty: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
580 |
assumes f: "positive M f" and b: "b \<in> sets M" and a: "a \<subseteq> b" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
581 |
shows "f b \<in> measure_set M f a" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
582 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
583 |
have "(f \<circ> (\<lambda>i. {})(0 := b)) sums setsum (f \<circ> (\<lambda>i. {})(0 := b)) {0..<1::nat}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
584 |
by (rule series_zero) (simp add: positive_imp_0 [OF f]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
585 |
also have "... = f b" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
586 |
by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
587 |
finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
588 |
thus ?thesis using a |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
589 |
by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"] |
35582 | 590 |
simp add: measure_set_def disjoint_family_on_def b split_if_mem2) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
591 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
592 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
593 |
lemma (in algebra) inf_measure_pos0: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
594 |
"positive M f \<Longrightarrow> x \<in> measure_set M f a \<Longrightarrow> 0 \<le> x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
595 |
apply (auto simp add: positive_def measure_set_def sums_iff intro!: suminf_ge_zero) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
596 |
apply blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
597 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
598 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
599 |
lemma (in algebra) inf_measure_pos: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
600 |
shows "positive M f \<Longrightarrow> x \<subseteq> space M \<Longrightarrow> 0 \<le> Inf (measure_set M f x)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
601 |
apply (rule Inf_greatest) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
602 |
apply (metis emptyE inf_measure_nonempty top) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
603 |
apply (metis inf_measure_pos0) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
604 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
605 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
606 |
lemma (in algebra) additive_increasing: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
607 |
assumes posf: "positive M f" and addf: "additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
608 |
shows "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
609 |
proof (auto simp add: increasing_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
610 |
fix x y |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
611 |
assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
612 |
have "f x \<le> f x + f (y-x)" using posf |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
613 |
by (simp add: positive_def) (metis Diff xy) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
614 |
also have "... = f (x \<union> (y-x))" using addf |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
615 |
by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
616 |
also have "... = f y" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
617 |
by (metis Un_Diff_cancel Un_absorb1 xy) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
618 |
finally show "f x \<le> f y" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
619 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
620 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
621 |
lemma (in algebra) countably_additive_additive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
622 |
assumes posf: "positive M f" and ca: "countably_additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
623 |
shows "additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
624 |
proof (auto simp add: additive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
625 |
fix x y |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
626 |
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
|
627 |
hence "disjoint_family (binaryset x y)" |
35582 | 628 |
by (auto simp add: disjoint_family_on_def binaryset_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
629 |
hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
630 |
(\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
631 |
f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
632 |
using ca |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
633 |
by (simp add: countably_additive_def) (metis UN_binaryset_eq sums_unique) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
634 |
hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
635 |
f (x \<union> y) = suminf (\<lambda>n. f (binaryset x y n))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
636 |
by (simp add: range_binaryset_eq UN_binaryset_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
637 |
thus "f (x \<union> y) = f x + f y" using posf x y |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
638 |
by (simp add: Un suminf_binaryset_eq positive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
639 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
640 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
641 |
lemma (in algebra) inf_measure_agrees: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
642 |
assumes posf: "positive M f" and ca: "countably_additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
643 |
and s: "s \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
644 |
shows "Inf (measure_set M f s) = f s" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
645 |
proof (rule Inf_eq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
646 |
fix z |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
647 |
assume z: "z \<in> measure_set M f s" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
648 |
from this obtain A where |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
649 |
A: "range A \<subseteq> sets M" and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
650 |
and "s \<subseteq> (\<Union>x. A x)" and sm: "summable (f \<circ> A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
651 |
and si: "suminf (f \<circ> A) = z" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
652 |
by (auto simp add: measure_set_def sums_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
653 |
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
|
654 |
have inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
655 |
by (metis additive_increasing ca countably_additive_additive posf) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
656 |
have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
657 |
proof (rule countably_additiveD [OF ca]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
658 |
show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s |
33536 | 659 |
by blast |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
660 |
show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj |
35582 | 661 |
by (auto simp add: disjoint_family_on_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
662 |
show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s |
33536 | 663 |
by (metis UN_extend_simps(4) s seq) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
664 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
665 |
hence "f s = suminf (\<lambda>i. f (A i \<inter> s))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
666 |
by (metis Int_commute UN_simps(4) seq sums_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
667 |
also have "... \<le> suminf (f \<circ> A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
668 |
proof (rule summable_le [OF _ _ sm]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
669 |
show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s |
33536 | 670 |
by (force intro: increasingD [OF inc]) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
671 |
show "summable (\<lambda>i. f (A i \<inter> s))" using sums |
33536 | 672 |
by (simp add: sums_iff) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
673 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
674 |
also have "... = z" by (rule si) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
675 |
finally show "f s \<le> z" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
676 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
677 |
fix y |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
678 |
assume y: "!!u. u \<in> measure_set M f s \<Longrightarrow> y \<le> u" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
679 |
thus "y \<le> f s" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
680 |
by (blast intro: inf_measure_nonempty [OF posf s subset_refl]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
681 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
682 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
683 |
lemma (in algebra) inf_measure_empty: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
684 |
assumes posf: "positive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
685 |
shows "Inf (measure_set M f {}) = 0" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
686 |
proof (rule antisym) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
687 |
show "0 \<le> Inf (measure_set M f {})" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
688 |
by (metis empty_subsetI inf_measure_pos posf) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
689 |
show "Inf (measure_set M f {}) \<le> 0" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
690 |
by (metis Inf_lower empty_sets inf_measure_pos0 inf_measure_nonempty posf |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
691 |
positive_imp_0 subset_refl) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
692 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
693 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
694 |
lemma (in algebra) inf_measure_positive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
695 |
"positive M f \<Longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
696 |
positive (| space = space M, sets = Pow (space M) |) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
697 |
(\<lambda>x. Inf (measure_set M f x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
698 |
by (simp add: positive_def inf_measure_empty inf_measure_pos) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
699 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
700 |
lemma (in algebra) inf_measure_increasing: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
701 |
assumes posf: "positive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
702 |
shows "increasing (| space = space M, sets = Pow (space M) |) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
703 |
(\<lambda>x. Inf (measure_set M f x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
704 |
apply (auto simp add: increasing_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
705 |
apply (rule Inf_greatest, metis emptyE inf_measure_nonempty top posf) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
706 |
apply (rule Inf_lower) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
707 |
apply (clarsimp simp add: measure_set_def, blast) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
708 |
apply (blast intro: inf_measure_pos0 posf) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
709 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
710 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
711 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
712 |
lemma (in algebra) inf_measure_le: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
713 |
assumes posf: "positive M f" and inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
714 |
and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M & s \<subseteq> (\<Union>i. A i) & (f \<circ> A) sums r}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
715 |
shows "Inf (measure_set M f s) \<le> x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
716 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
717 |
from x |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
718 |
obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
719 |
and sm: "summable (f \<circ> A)" and xeq: "suminf (f \<circ> A) = x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
720 |
by (auto simp add: sums_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
721 |
have dA: "range (disjointed A) \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
722 |
by (metis A range_disjointed_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
723 |
have "\<forall>n. \<bar>(f o disjointed A) n\<bar> \<le> (f \<circ> A) n" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
724 |
proof (auto) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
725 |
fix n |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
726 |
have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA |
33536 | 727 |
by (auto simp add: positive_def image_subset_iff) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
728 |
also have "... \<le> f (A n)" |
33536 | 729 |
by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
730 |
finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
731 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
732 |
from Series.summable_le2 [OF this sm] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
733 |
have sda: "summable (f o disjointed A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
734 |
"suminf (f o disjointed A) \<le> suminf (f \<circ> A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
735 |
by blast+ |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
736 |
hence ley: "suminf (f o disjointed A) \<le> x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
737 |
by (metis xeq) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
738 |
from sda have "(f \<circ> disjointed A) sums suminf (f \<circ> disjointed A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
739 |
by (simp add: sums_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
740 |
hence y: "suminf (f o disjointed A) \<in> measure_set M f s" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
741 |
apply (auto simp add: measure_set_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
742 |
apply (rule_tac x="disjointed A" in exI) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
743 |
apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
744 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
745 |
show ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
746 |
by (blast intro: Inf_lower y order_trans [OF _ ley] inf_measure_pos0 posf) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
747 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
748 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
749 |
lemma (in algebra) inf_measure_close: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
750 |
assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
751 |
shows "\<exists>A l. range A \<subseteq> sets M & disjoint_family A & s \<subseteq> (\<Union>i. A i) & |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
752 |
(f \<circ> A) sums l & l \<le> Inf (measure_set M f s) + e" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
753 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
754 |
have " measure_set M f s \<noteq> {}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
755 |
by (metis emptyE ss inf_measure_nonempty [OF posf top]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
756 |
hence "\<exists>l \<in> measure_set M f s. l < Inf (measure_set M f s) + e" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
757 |
by (rule Inf_close [OF _ e]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
758 |
thus ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
759 |
by (auto simp add: measure_set_def, rule_tac x=" A" in exI, auto) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
760 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
761 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
762 |
lemma (in algebra) inf_measure_countably_subadditive: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
763 |
assumes posf: "positive M f" and inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
764 |
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
|
765 |
(\<lambda>x. Inf (measure_set M f x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
766 |
proof (auto simp add: countably_subadditive_def o_def, rule field_le_epsilon) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
767 |
fix A :: "nat \<Rightarrow> 'a set" and e :: real |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
768 |
assume A: "range A \<subseteq> Pow (space M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
769 |
and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
770 |
and sb: "(\<Union>i. A i) \<subseteq> space M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
771 |
and sum1: "summable (\<lambda>n. Inf (measure_set M f (A n)))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
772 |
and e: "0 < e" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
773 |
have "!!n. \<exists>B l. range B \<subseteq> sets M \<and> disjoint_family B \<and> A n \<subseteq> (\<Union>i. B i) \<and> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
774 |
(f o B) sums l \<and> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
775 |
l \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
776 |
apply (rule inf_measure_close [OF posf]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
777 |
apply (metis e half mult_pos_pos zero_less_power) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
778 |
apply (metis UNIV_I UN_subset_iff sb) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
779 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
780 |
hence "\<exists>BB ll. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
781 |
A n \<subseteq> (\<Union>i. BB n i) \<and> (f o BB n) sums ll n \<and> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
782 |
ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
783 |
by (rule choice2) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
784 |
then obtain BB ll |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
785 |
where BB: "!!n. (range (BB n) \<subseteq> sets M)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
786 |
and disjBB: "!!n. disjoint_family (BB n)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
787 |
and sbBB: "!!n. A n \<subseteq> (\<Union>i. BB n i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
788 |
and BBsums: "!!n. (f o BB n) sums ll n" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
789 |
and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
790 |
by auto blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
791 |
have llpos: "!!n. 0 \<le> ll n" |
33536 | 792 |
by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
793 |
range_subsetD BB) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
794 |
have sll: "summable ll & |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
795 |
suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
796 |
proof - |
33536 | 797 |
have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)" |
798 |
by (rule sums_mult [OF power_half_series]) |
|
799 |
hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)" |
|
800 |
and eqe: "(\<Sum>n. e * (1 / 2) ^ n / 2) = e" |
|
801 |
by (auto simp add: sums_iff) |
|
802 |
have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) + |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
803 |
suminf (\<lambda>n. e * (1/2)^(Suc n)) = |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
804 |
suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))" |
33536 | 805 |
by (rule suminf_add [OF sum1 sum0]) |
806 |
have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n" |
|
807 |
by (metis ll llpos abs_of_nonneg) |
|
808 |
have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))" |
|
809 |
by (rule summable_add [OF sum1 sum0]) |
|
810 |
have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)" |
|
811 |
using Series.summable_le2 [OF 1 2] by auto |
|
812 |
also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
813 |
(\<Sum>n. e * (1 / 2) ^ Suc n)" |
33536 | 814 |
by (metis 0) |
815 |
also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e" |
|
816 |
by (simp add: eqe) |
|
817 |
finally show ?thesis using Series.summable_le2 [OF 1 2] by auto |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
818 |
qed |
35704
5007843dae33
convert HOL-Probability to use Nat_Bijection library
huffman
parents:
35582
diff
changeset
|
819 |
def C \<equiv> "(split BB) o prod_decode" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
820 |
have C: "!!n. C n \<in> sets M" |
35704
5007843dae33
convert HOL-Probability to use Nat_Bijection library
huffman
parents:
35582
diff
changeset
|
821 |
apply (rule_tac p="prod_decode n" in PairE) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
822 |
apply (simp add: C_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
823 |
apply (metis BB subsetD rangeI) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
824 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
825 |
have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
826 |
proof (auto simp add: C_def) |
33536 | 827 |
fix x i |
828 |
assume x: "x \<in> A i" |
|
829 |
with sbBB [of i] obtain j where "x \<in> BB i j" |
|
830 |
by blast |
|
35704
5007843dae33
convert HOL-Probability to use Nat_Bijection library
huffman
parents:
35582
diff
changeset
|
831 |
thus "\<exists>i. x \<in> split BB (prod_decode i)" |
5007843dae33
convert HOL-Probability to use Nat_Bijection library
huffman
parents:
35582
diff
changeset
|
832 |
by (metis prod_encode_inverse prod.cases prod_case_split) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
833 |
qed |
35704
5007843dae33
convert HOL-Probability to use Nat_Bijection library
huffman
parents:
35582
diff
changeset
|
834 |
have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
835 |
by (rule ext) (auto simp add: C_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
836 |
also have "... sums suminf ll" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
837 |
proof (rule suminf_2dimen) |
33536 | 838 |
show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB |
839 |
by (force simp add: positive_def) |
|
840 |
show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB |
|
841 |
by (force simp add: o_def) |
|
842 |
show "summable ll" using sll |
|
843 |
by auto |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
844 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
845 |
finally have Csums: "(f \<circ> C) sums suminf ll" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
846 |
have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
847 |
apply (rule inf_measure_le [OF posf inc], auto) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
848 |
apply (rule_tac x="C" in exI) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
849 |
apply (auto simp add: C sbC Csums) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
850 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
851 |
also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
852 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
853 |
finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
854 |
(\<Sum>n. Inf (measure_set M f (A n))) + e" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
855 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
856 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
857 |
lemma (in algebra) inf_measure_outer: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
858 |
"positive M f \<Longrightarrow> increasing M f |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
859 |
\<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
860 |
(\<lambda>x. Inf (measure_set M f x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
861 |
by (simp add: outer_measure_space_def inf_measure_positive |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
862 |
inf_measure_increasing inf_measure_countably_subadditive) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
863 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
864 |
(*MOVE UP*) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
865 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
866 |
lemma (in algebra) algebra_subset_lambda_system: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
867 |
assumes posf: "positive M f" and inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
868 |
and add: "additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
869 |
shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
870 |
(\<lambda>x. Inf (measure_set M f x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
871 |
proof (auto dest: sets_into_space |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
872 |
simp add: algebra.lambda_system_eq [OF algebra_Pow]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
873 |
fix x s |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
874 |
assume x: "x \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
875 |
and s: "s \<subseteq> space M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
876 |
have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
877 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
878 |
have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
879 |
\<le> Inf (measure_set M f s)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
880 |
proof (rule field_le_epsilon) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
881 |
fix e :: real |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
882 |
assume e: "0 < e" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
883 |
from inf_measure_close [OF posf e s] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
884 |
obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
885 |
and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l" |
33536 | 886 |
and l: "l \<le> Inf (measure_set M f s) + e" |
887 |
by auto |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
888 |
have [simp]: "!!x. x \<in> sets M \<Longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
889 |
(f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)" |
33536 | 890 |
by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
891 |
have [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)" |
33536 | 892 |
by (subst additiveD [OF add, symmetric]) |
893 |
(auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
894 |
have fsumb: "summable (f \<circ> A)" |
33536 | 895 |
by (metis fsums sums_iff) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
896 |
{ fix u |
33536 | 897 |
assume u: "u \<in> sets M" |
898 |
have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)" |
|
899 |
by (simp add: positive_imp_pos [OF posf] increasingD [OF inc] |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
900 |
u Int range_subsetD [OF A]) |
33536 | 901 |
have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
902 |
by (rule summable_comparison_test [OF _ fsumb]) simp |
33536 | 903 |
have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
904 |
proof (rule Inf_lower) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
905 |
show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
906 |
apply (simp add: measure_set_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
907 |
apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
908 |
apply (auto simp add: disjoint_family_subset [OF disj]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
909 |
apply (blast intro: u range_subsetD [OF A]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
910 |
apply (blast dest: subsetD [OF sUN]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
911 |
apply (metis 1 o_assoc sums_iff) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
912 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
913 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
914 |
show "\<And>x. x \<in> measure_set M f (s \<inter> u) \<Longrightarrow> 0 \<le> x" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
915 |
by (blast intro: inf_measure_pos0 [OF posf]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
916 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
917 |
note 1 2 |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
918 |
} note lesum = this |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
919 |
have sum1: "summable (f o (\<lambda>z. z\<inter>x) o A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
920 |
and inf1: "Inf (measure_set M f (s\<inter>x)) \<le> suminf (f o (\<lambda>z. z\<inter>x) o A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
921 |
and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
922 |
and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
923 |
\<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)" |
33536 | 924 |
by (metis Diff lesum top x)+ |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
925 |
hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
926 |
\<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)" |
33536 | 927 |
by (simp add: x) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
928 |
also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] |
33536 | 929 |
by (simp add: x) (simp add: o_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
930 |
also have "... \<le> Inf (measure_set M f s) + e" |
33536 | 931 |
by (metis fsums l sums_unique) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
932 |
finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
933 |
\<le> Inf (measure_set M f s) + e" . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
934 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
935 |
moreover |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
936 |
have "Inf (measure_set M f s) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
937 |
\<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
938 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
939 |
have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
940 |
by (metis Un_Diff_Int Un_commute) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
941 |
also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
942 |
apply (rule subadditiveD) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
943 |
apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow |
33536 | 944 |
inf_measure_positive inf_measure_countably_subadditive posf inc) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
945 |
apply (auto simp add: subsetD [OF s]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
946 |
done |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
947 |
finally show ?thesis . |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
948 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
949 |
ultimately |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
950 |
show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x)) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
951 |
= Inf (measure_set M f s)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
952 |
by (rule order_antisym) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
953 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
954 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
955 |
lemma measure_down: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
956 |
"measure_space N \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
957 |
(measure M = measure N) \<Longrightarrow> measure_space M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
958 |
by (simp add: measure_space_def measure_space_axioms_def positive_def |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
959 |
countably_additive_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
960 |
blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
961 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
962 |
theorem (in algebra) caratheodory: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
963 |
assumes posf: "positive M f" and ca: "countably_additive M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
964 |
shows "\<exists>MS :: 'a measure_space. |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
965 |
(\<forall>s \<in> sets M. measure MS s = f s) \<and> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
966 |
((|space = space MS, sets = sets MS|) = sigma (space M) (sets M)) \<and> |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
967 |
measure_space MS" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
968 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
969 |
have inc: "increasing M f" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
970 |
by (metis additive_increasing ca countably_additive_additive posf) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
971 |
let ?infm = "(\<lambda>x. Inf (measure_set M f x))" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
972 |
def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
973 |
have mls: "measure_space (|space = space M, sets = ls, measure = ?infm|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
974 |
using sigma_algebra.caratheodory_lemma |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
975 |
[OF sigma_algebra_Pow inf_measure_outer [OF posf inc]] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
976 |
by (simp add: ls_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
977 |
hence sls: "sigma_algebra (|space = space M, sets = ls, measure = ?infm|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
978 |
by (simp add: measure_space_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
979 |
have "sets M \<subseteq> ls" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
980 |
by (simp add: ls_def) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
981 |
(metis ca posf inc countably_additive_additive algebra_subset_lambda_system) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
982 |
hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
983 |
using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"] |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
984 |
by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
985 |
have "measure_space (|space = space M, |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
986 |
sets = sigma_sets (space M) (sets M), |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
987 |
measure = ?infm|)" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
988 |
by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
989 |
(simp_all add: sgs_sb space_closed) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
990 |
thus ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
991 |
by (force simp add: sigma_def inf_measure_agrees [OF posf ca]) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
992 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
993 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
994 |
end |