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