author | hoelzl |
Fri, 21 Jan 2011 11:39:26 +0100 | |
changeset 41660 | 7795aaab6038 |
parent 41545 | 9c869baf1c66 |
child 41661 | baf1964bc468 |
permissions | -rw-r--r-- |
40859 | 1 |
(* Author: Lawrence C Paulson; Armin Heller, Johannes Hoelzl, TU Muenchen *) |
33271
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 Measure |
38656 | 4 |
imports Caratheodory |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
5 |
begin |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
6 |
|
40859 | 7 |
lemma inj_on_image_eq_iff: |
8 |
assumes "inj_on f S" |
|
9 |
assumes "A \<subseteq> S" "B \<subseteq> S" |
|
10 |
shows "(f ` A = f ` B) \<longleftrightarrow> (A = B)" |
|
11 |
proof - |
|
12 |
have "inj_on f (A \<union> B)" |
|
13 |
using assms by (auto intro: subset_inj_on) |
|
14 |
from inj_on_Un_image_eq_iff[OF this] |
|
15 |
show ?thesis . |
|
16 |
qed |
|
17 |
||
18 |
lemma image_vimage_inter_eq: |
|
19 |
assumes "f ` S = T" "X \<subseteq> T" |
|
20 |
shows "f ` (f -` X \<inter> S) = X" |
|
21 |
proof (intro antisym) |
|
22 |
have "f ` (f -` X \<inter> S) \<subseteq> f ` (f -` X)" by auto |
|
23 |
also have "\<dots> = X \<inter> range f" by simp |
|
24 |
also have "\<dots> = X" using assms by auto |
|
25 |
finally show "f ` (f -` X \<inter> S) \<subseteq> X" by auto |
|
26 |
next |
|
27 |
show "X \<subseteq> f ` (f -` X \<inter> S)" |
|
28 |
proof |
|
29 |
fix x assume "x \<in> X" |
|
30 |
then have "x \<in> T" using `X \<subseteq> T` by auto |
|
31 |
then obtain y where "x = f y" "y \<in> S" |
|
32 |
using assms by auto |
|
33 |
then have "{y} \<subseteq> f -` X \<inter> S" using `x \<in> X` by auto |
|
34 |
moreover have "x \<in> f ` {y}" using `x = f y` by auto |
|
35 |
ultimately show "x \<in> f ` (f -` X \<inter> S)" by auto |
|
36 |
qed |
|
37 |
qed |
|
38 |
||
39 |
text {* |
|
40 |
This formalisation of measure theory is based on the work of Hurd/Coble wand |
|
41 |
was later translated by Lawrence Paulson to Isabelle/HOL. Later it was |
|
42 |
modified to use the positive infinite reals and to prove the uniqueness of |
|
43 |
cut stable measures. |
|
44 |
*} |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
45 |
|
38656 | 46 |
section {* Equations for the measure function @{text \<mu>} *} |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
47 |
|
38656 | 48 |
lemma (in measure_space) measure_countably_additive: |
49 |
assumes "range A \<subseteq> sets M" "disjoint_family A" |
|
50 |
shows "psuminf (\<lambda>i. \<mu> (A i)) = \<mu> (\<Union>i. A i)" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
51 |
proof - |
38656 | 52 |
have "(\<Union> i. A i) \<in> sets M" using assms(1) by (rule countable_UN) |
53 |
with ca assms show ?thesis by (simp add: countably_additive_def) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
54 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
55 |
|
38656 | 56 |
lemma (in measure_space) measure_space_cong: |
57 |
assumes "\<And>A. A \<in> sets M \<Longrightarrow> \<nu> A = \<mu> A" |
|
58 |
shows "measure_space M \<nu>" |
|
59 |
proof |
|
60 |
show "\<nu> {} = 0" using assms by auto |
|
61 |
show "countably_additive M \<nu>" unfolding countably_additive_def |
|
62 |
proof safe |
|
63 |
fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" |
|
64 |
then have "\<And>i. A i \<in> sets M" "(UNION UNIV A) \<in> sets M" by auto |
|
65 |
from this[THEN assms] measure_countably_additive[OF A] |
|
66 |
show "(\<Sum>\<^isub>\<infinity>n. \<nu> (A n)) = \<nu> (UNION UNIV A)" by simp |
|
67 |
qed |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
68 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
69 |
|
38656 | 70 |
lemma (in measure_space) additive: "additive M \<mu>" |
71 |
proof (rule algebra.countably_additive_additive [OF _ _ ca]) |
|
72 |
show "algebra M" by default |
|
73 |
show "positive \<mu>" by (simp add: positive_def) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
74 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
75 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
76 |
lemma (in measure_space) measure_additive: |
38656 | 77 |
"a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} |
78 |
\<Longrightarrow> \<mu> a + \<mu> b = \<mu> (a \<union> b)" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
79 |
by (metis additiveD additive) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
80 |
|
36624 | 81 |
lemma (in measure_space) measure_mono: |
82 |
assumes "a \<subseteq> b" "a \<in> sets M" "b \<in> sets M" |
|
38656 | 83 |
shows "\<mu> a \<le> \<mu> b" |
36624 | 84 |
proof - |
85 |
have "b = a \<union> (b - a)" using assms by auto |
|
86 |
moreover have "{} = a \<inter> (b - a)" by auto |
|
38656 | 87 |
ultimately have "\<mu> b = \<mu> a + \<mu> (b - a)" |
36624 | 88 |
using measure_additive[of a "b - a"] local.Diff[of b a] assms by auto |
38656 | 89 |
moreover have "\<mu> (b - a) \<ge> 0" using assms by auto |
90 |
ultimately show "\<mu> a \<le> \<mu> b" by auto |
|
36624 | 91 |
qed |
92 |
||
38656 | 93 |
lemma (in measure_space) measure_compl: |
94 |
assumes s: "s \<in> sets M" and fin: "\<mu> s \<noteq> \<omega>" |
|
95 |
shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
96 |
proof - |
38656 | 97 |
have s_less_space: "\<mu> s \<le> \<mu> (space M)" |
98 |
using s by (auto intro!: measure_mono sets_into_space) |
|
99 |
||
100 |
have "\<mu> (space M) = \<mu> (s \<union> (space M - s))" using s |
|
101 |
by (metis Un_Diff_cancel Un_absorb1 s sets_into_space) |
|
102 |
also have "... = \<mu> s + \<mu> (space M - s)" |
|
103 |
by (rule additiveD [OF additive]) (auto simp add: s) |
|
104 |
finally have "\<mu> (space M) = \<mu> s + \<mu> (space M - s)" . |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
105 |
thus ?thesis |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
106 |
unfolding minus_pextreal_eq2[OF s_less_space fin] |
38656 | 107 |
by (simp add: ac_simps) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
108 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
109 |
|
38656 | 110 |
lemma (in measure_space) measure_Diff: |
111 |
assumes finite: "\<mu> B \<noteq> \<omega>" |
|
112 |
and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A" |
|
113 |
shows "\<mu> (A - B) = \<mu> A - \<mu> B" |
|
114 |
proof - |
|
115 |
have *: "(A - B) \<union> B = A" using `B \<subseteq> A` by auto |
|
116 |
||
117 |
have "\<mu> ((A - B) \<union> B) = \<mu> (A - B) + \<mu> B" |
|
118 |
using measurable by (rule_tac measure_additive[symmetric]) auto |
|
119 |
thus ?thesis unfolding * using `\<mu> B \<noteq> \<omega>` |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
120 |
by (simp add: pextreal_cancel_plus_minus) |
38656 | 121 |
qed |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
122 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
123 |
lemma (in measure_space) measure_countable_increasing: |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
124 |
assumes A: "range A \<subseteq> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
125 |
and A0: "A 0 = {}" |
38656 | 126 |
and ASuc: "\<And>n. A n \<subseteq> A (Suc n)" |
127 |
shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
128 |
proof - |
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 |
fix n |
38656 | 131 |
have "\<mu> (A n) = |
132 |
setsum (\<mu> \<circ> (\<lambda>i. A (Suc i) - A i)) {..<n}" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
133 |
proof (induct n) |
37032 | 134 |
case 0 thus ?case by (auto simp add: A0) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
135 |
next |
38656 | 136 |
case (Suc m) |
33536 | 137 |
have "A (Suc m) = A m \<union> (A (Suc m) - A m)" |
138 |
by (metis ASuc Un_Diff_cancel Un_absorb1) |
|
38656 | 139 |
hence "\<mu> (A (Suc m)) = |
140 |
\<mu> (A m) + \<mu> (A (Suc m) - A m)" |
|
141 |
by (subst measure_additive) |
|
142 |
(auto simp add: measure_additive range_subsetD [OF A]) |
|
33536 | 143 |
with Suc show ?case |
144 |
by simp |
|
38656 | 145 |
qed } |
146 |
note Meq = this |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
147 |
have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)" |
38656 | 148 |
proof (rule UN_finite2_eq [where k=1], simp) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
149 |
fix i |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
150 |
show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)" |
33536 | 151 |
proof (induct i) |
152 |
case 0 thus ?case by (simp add: A0) |
|
153 |
next |
|
38656 | 154 |
case (Suc i) |
33536 | 155 |
thus ?case |
156 |
by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc]) |
|
157 |
qed |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
158 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
159 |
have A1: "\<And>i. A (Suc i) - A i \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
160 |
by (metis A Diff range_subsetD) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
161 |
have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M" |
37032 | 162 |
by (blast intro: range_subsetD [OF A]) |
38656 | 163 |
have "psuminf ( (\<lambda>i. \<mu> (A (Suc i) - A i))) = \<mu> (\<Union>i. A (Suc i) - A i)" |
164 |
by (rule measure_countably_additive) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
165 |
(auto simp add: disjoint_family_Suc ASuc A1 A2) |
38656 | 166 |
also have "... = \<mu> (\<Union>i. A i)" |
167 |
by (simp add: Aeq) |
|
168 |
finally have "psuminf (\<lambda>i. \<mu> (A (Suc i) - A i)) = \<mu> (\<Union>i. A i)" . |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
169 |
thus ?thesis |
38656 | 170 |
by (auto simp add: Meq psuminf_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
171 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
172 |
|
38656 | 173 |
lemma (in measure_space) continuity_from_below: |
174 |
assumes A: "range A \<subseteq> sets M" |
|
175 |
and ASuc: "!!n. A n \<subseteq> A (Suc n)" |
|
176 |
shows "(SUP n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
|
177 |
proof - |
|
178 |
have *: "(SUP n. \<mu> (nat_case {} A (Suc n))) = (SUP n. \<mu> (nat_case {} A n))" |
|
179 |
apply (rule Sup_mono_offset_Suc) |
|
180 |
apply (rule measure_mono) |
|
181 |
using assms by (auto split: nat.split) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
182 |
|
38656 | 183 |
have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)" |
184 |
by (auto simp add: split: nat.splits) |
|
185 |
have meq: "\<And>n. \<mu> (A n) = (\<mu> \<circ> nat_case {} A) (Suc n)" |
|
186 |
by simp |
|
187 |
have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. nat_case {} A i)" |
|
188 |
by (rule measure_countable_increasing) |
|
189 |
(auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) |
|
190 |
also have "\<mu> (\<Union>i. nat_case {} A i) = \<mu> (\<Union>i. A i)" |
|
191 |
by (simp add: ueq) |
|
192 |
finally have "(SUP n. \<mu> (nat_case {} A n)) = \<mu> (\<Union>i. A i)" . |
|
193 |
thus ?thesis unfolding meq * comp_def . |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
194 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
195 |
|
38656 | 196 |
lemma (in measure_space) measure_up: |
40859 | 197 |
assumes "\<And>i. B i \<in> sets M" "B \<up> P" |
38656 | 198 |
shows "(\<lambda>i. \<mu> (B i)) \<up> \<mu> P" |
199 |
using assms unfolding isoton_def |
|
200 |
by (auto intro!: measure_mono continuity_from_below) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
201 |
|
40859 | 202 |
lemma (in measure_space) continuity_from_below': |
203 |
assumes A: "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)" |
|
204 |
shows "(\<lambda>i. (\<mu> (A i))) ----> (\<mu> (\<Union>i. A i))" |
|
205 |
proof- let ?A = "\<Union>i. A i" |
|
206 |
have " (\<lambda>i. \<mu> (A i)) \<up> \<mu> ?A" apply(rule measure_up) |
|
207 |
using assms unfolding complete_lattice_class.isoton_def by auto |
|
208 |
thus ?thesis by(rule isotone_Lim(1)) |
|
209 |
qed |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
210 |
|
38656 | 211 |
lemma (in measure_space) continuity_from_above: |
212 |
assumes A: "range A \<subseteq> sets M" |
|
213 |
and mono_Suc: "\<And>n. A (Suc n) \<subseteq> A n" |
|
214 |
and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>" |
|
215 |
shows "(INF n. \<mu> (A n)) = \<mu> (\<Inter>i. A i)" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
216 |
proof - |
38656 | 217 |
{ fix n have "A n \<subseteq> A 0" using mono_Suc by (induct n) auto } |
218 |
note mono = this |
|
219 |
||
220 |
have le_MI: "\<mu> (\<Inter>i. A i) \<le> \<mu> (A 0)" |
|
221 |
using A by (auto intro!: measure_mono) |
|
222 |
hence *: "\<mu> (\<Inter>i. A i) \<noteq> \<omega>" using finite[of 0] by auto |
|
223 |
||
224 |
have le_IM: "(INF n. \<mu> (A n)) \<le> \<mu> (A 0)" |
|
225 |
by (rule INF_leI) simp |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
226 |
|
38656 | 227 |
have "\<mu> (A 0) - (INF n. \<mu> (A n)) = (SUP n. \<mu> (A 0 - A n))" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
228 |
unfolding pextreal_SUP_minus[symmetric] |
38656 | 229 |
using mono A finite by (subst measure_Diff) auto |
230 |
also have "\<dots> = \<mu> (\<Union>i. A 0 - A i)" |
|
231 |
proof (rule continuity_from_below) |
|
232 |
show "range (\<lambda>n. A 0 - A n) \<subseteq> sets M" |
|
233 |
using A by auto |
|
234 |
show "\<And>n. A 0 - A n \<subseteq> A 0 - A (Suc n)" |
|
235 |
using mono_Suc by auto |
|
236 |
qed |
|
237 |
also have "\<dots> = \<mu> (A 0) - \<mu> (\<Inter>i. A i)" |
|
238 |
using mono A finite * by (simp, subst measure_Diff) auto |
|
239 |
finally show ?thesis |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
240 |
by (rule pextreal_diff_eq_diff_imp_eq[OF finite[of 0] le_IM le_MI]) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
241 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
242 |
|
38656 | 243 |
lemma (in measure_space) measure_down: |
40859 | 244 |
assumes "\<And>i. B i \<in> sets M" "B \<down> P" |
38656 | 245 |
and finite: "\<And>i. \<mu> (B i) \<noteq> \<omega>" |
246 |
shows "(\<lambda>i. \<mu> (B i)) \<down> \<mu> P" |
|
247 |
using assms unfolding antiton_def |
|
248 |
by (auto intro!: measure_mono continuity_from_above) |
|
249 |
lemma (in measure_space) measure_insert: |
|
250 |
assumes sets: "{x} \<in> sets M" "A \<in> sets M" and "x \<notin> A" |
|
251 |
shows "\<mu> (insert x A) = \<mu> {x} + \<mu> A" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
252 |
proof - |
38656 | 253 |
have "{x} \<inter> A = {}" using `x \<notin> A` by auto |
254 |
from measure_additive[OF sets this] show ?thesis by simp |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
255 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
256 |
|
38656 | 257 |
lemma (in measure_space) measure_finite_singleton: |
258 |
assumes fin: "finite S" |
|
259 |
and ssets: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M" |
|
260 |
shows "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})" |
|
261 |
using assms proof induct |
|
262 |
case (insert x S) |
|
263 |
have *: "\<mu> S = (\<Sum>x\<in>S. \<mu> {x})" "{x} \<in> sets M" |
|
264 |
using insert.prems by (blast intro!: insert.hyps(3))+ |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
265 |
|
38656 | 266 |
have "(\<Union>x\<in>S. {x}) \<in> sets M" |
267 |
using insert.prems `finite S` by (blast intro!: finite_UN) |
|
268 |
hence "S \<in> sets M" by auto |
|
269 |
from measure_insert[OF `{x} \<in> sets M` this `x \<notin> S`] |
|
270 |
show ?case using `x \<notin> S` `finite S` * by simp |
|
271 |
qed simp |
|
35582 | 272 |
|
273 |
lemma (in measure_space) measure_finitely_additive': |
|
38656 | 274 |
assumes "f \<in> ({..< n :: nat} \<rightarrow> sets M)" |
35582 | 275 |
assumes "\<And> a b. \<lbrakk>a < n ; b < n ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}" |
38656 | 276 |
assumes "s = \<Union> (f ` {..< n})" |
277 |
shows "(\<Sum>i<n. (\<mu> \<circ> f) i) = \<mu> s" |
|
35582 | 278 |
proof - |
279 |
def f' == "\<lambda> i. (if i < n then f i else {})" |
|
38656 | 280 |
have rf: "range f' \<subseteq> sets M" unfolding f'_def |
35582 | 281 |
using assms empty_sets by auto |
38656 | 282 |
have df: "disjoint_family f'" unfolding f'_def disjoint_family_on_def |
35582 | 283 |
using assms by simp |
38656 | 284 |
have "\<Union> range f' = (\<Union> i \<in> {..< n}. f i)" |
35582 | 285 |
unfolding f'_def by auto |
38656 | 286 |
then have "\<mu> s = \<mu> (\<Union> range f')" |
35582 | 287 |
using assms by simp |
38656 | 288 |
then have part1: "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = \<mu> s" |
35582 | 289 |
using df rf ca[unfolded countably_additive_def, rule_format, of f'] |
290 |
by auto |
|
291 |
||
38656 | 292 |
have "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = (\<Sum> i< n. \<mu> (f' i))" |
293 |
by (rule psuminf_finite) (simp add: f'_def) |
|
294 |
also have "\<dots> = (\<Sum>i<n. \<mu> (f i))" |
|
35582 | 295 |
unfolding f'_def by auto |
38656 | 296 |
finally have part2: "(\<Sum>\<^isub>\<infinity> i. \<mu> (f' i)) = (\<Sum>i<n. \<mu> (f i))" by simp |
297 |
show ?thesis using part1 part2 by auto |
|
35582 | 298 |
qed |
299 |
||
300 |
||
301 |
lemma (in measure_space) measure_finitely_additive: |
|
302 |
assumes "finite r" |
|
303 |
assumes "r \<subseteq> sets M" |
|
304 |
assumes d: "\<And> a b. \<lbrakk>a \<in> r ; b \<in> r ; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<inter> b = {}" |
|
38656 | 305 |
shows "(\<Sum> i \<in> r. \<mu> i) = \<mu> (\<Union> r)" |
35582 | 306 |
using assms |
307 |
proof - |
|
308 |
(* counting the elements in r is enough *) |
|
38656 | 309 |
let ?R = "{..<card r}" |
35582 | 310 |
obtain f where f: "f ` ?R = r" "inj_on f ?R" |
311 |
using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite r`] |
|
38656 | 312 |
unfolding atLeast0LessThan by auto |
35582 | 313 |
hence f_into_sets: "f \<in> ?R \<rightarrow> sets M" using assms by auto |
314 |
have disj: "\<And> a b. \<lbrakk>a \<in> ?R ; b \<in> ?R ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}" |
|
315 |
proof - |
|
316 |
fix a b assume asm: "a \<in> ?R" "b \<in> ?R" "a \<noteq> b" |
|
317 |
hence neq: "f a \<noteq> f b" using f[unfolded inj_on_def, rule_format] by blast |
|
318 |
from asm have "f a \<in> r" "f b \<in> r" using f by auto |
|
319 |
thus "f a \<inter> f b = {}" using d[of "f a" "f b"] f using neq by auto |
|
320 |
qed |
|
321 |
have "(\<Union> r) = (\<Union> i \<in> ?R. f i)" |
|
322 |
using f by auto |
|
38656 | 323 |
hence "\<mu> (\<Union> r)= \<mu> (\<Union> i \<in> ?R. f i)" by simp |
324 |
also have "\<dots> = (\<Sum> i \<in> ?R. \<mu> (f i))" |
|
35582 | 325 |
using measure_finitely_additive'[OF f_into_sets disj] by simp |
38656 | 326 |
also have "\<dots> = (\<Sum> a \<in> r. \<mu> a)" |
327 |
using f[rule_format] setsum_reindex[of f ?R "\<lambda> a. \<mu> a"] by auto |
|
35582 | 328 |
finally show ?thesis by simp |
329 |
qed |
|
330 |
||
331 |
lemma (in measure_space) measure_finitely_additive'': |
|
332 |
assumes "finite s" |
|
333 |
assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<in> sets M" |
|
334 |
assumes d: "disjoint_family_on a s" |
|
38656 | 335 |
shows "(\<Sum> i \<in> s. \<mu> (a i)) = \<mu> (\<Union> i \<in> s. a i)" |
35582 | 336 |
using assms |
337 |
proof - |
|
338 |
(* counting the elements in s is enough *) |
|
38656 | 339 |
let ?R = "{..< card s}" |
35582 | 340 |
obtain f where f: "f ` ?R = s" "inj_on f ?R" |
341 |
using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite s`] |
|
38656 | 342 |
unfolding atLeast0LessThan by auto |
35582 | 343 |
hence f_into_sets: "a \<circ> f \<in> ?R \<rightarrow> sets M" using assms unfolding o_def by auto |
344 |
have disj: "\<And> i j. \<lbrakk>i \<in> ?R ; j \<in> ?R ; i \<noteq> j\<rbrakk> \<Longrightarrow> (a \<circ> f) i \<inter> (a \<circ> f) j = {}" |
|
345 |
proof - |
|
346 |
fix i j assume asm: "i \<in> ?R" "j \<in> ?R" "i \<noteq> j" |
|
347 |
hence neq: "f i \<noteq> f j" using f[unfolded inj_on_def, rule_format] by blast |
|
348 |
from asm have "f i \<in> s" "f j \<in> s" using f by auto |
|
349 |
thus "(a \<circ> f) i \<inter> (a \<circ> f) j = {}" |
|
350 |
using d f neq unfolding disjoint_family_on_def by auto |
|
351 |
qed |
|
352 |
have "(\<Union> i \<in> s. a i) = (\<Union> i \<in> f ` ?R. a i)" using f by auto |
|
353 |
hence "(\<Union> i \<in> s. a i) = (\<Union> i \<in> ?R. a (f i))" by auto |
|
38656 | 354 |
hence "\<mu> (\<Union> i \<in> s. a i) = (\<Sum> i \<in> ?R. \<mu> (a (f i)))" |
35582 | 355 |
using measure_finitely_additive'[OF f_into_sets disj] by simp |
38656 | 356 |
also have "\<dots> = (\<Sum> i \<in> s. \<mu> (a i))" |
357 |
using f[rule_format] setsum_reindex[of f ?R "\<lambda> i. \<mu> (a i)"] by auto |
|
35582 | 358 |
finally show ?thesis by simp |
359 |
qed |
|
360 |
||
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
361 |
lemma (in sigma_algebra) finite_additivity_sufficient: |
38656 | 362 |
assumes fin: "finite (space M)" and pos: "positive \<mu>" and add: "additive M \<mu>" |
363 |
shows "measure_space M \<mu>" |
|
364 |
proof |
|
365 |
show [simp]: "\<mu> {} = 0" using pos by (simp add: positive_def) |
|
366 |
show "countably_additive M \<mu>" |
|
367 |
proof (auto simp add: countably_additive_def) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
368 |
fix A :: "nat \<Rightarrow> 'a set" |
38656 | 369 |
assume A: "range A \<subseteq> sets M" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
370 |
and disj: "disjoint_family A" |
38656 | 371 |
and UnA: "(\<Union>i. A i) \<in> sets M" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
372 |
def I \<equiv> "{i. A i \<noteq> {}}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
373 |
have "Union (A ` I) \<subseteq> space M" using A |
38656 | 374 |
by auto (metis range_subsetD subsetD sets_into_space) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
375 |
hence "finite (A ` I)" |
38656 | 376 |
by (metis finite_UnionD finite_subset fin) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
377 |
moreover have "inj_on A I" using disj |
38656 | 378 |
by (auto simp add: I_def disjoint_family_on_def inj_on_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
379 |
ultimately have finI: "finite I" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
380 |
by (metis finite_imageD) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
381 |
hence "\<exists>N. \<forall>m\<ge>N. A m = {}" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
382 |
proof (cases "I = {}") |
38656 | 383 |
case True thus ?thesis by (simp add: I_def) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
384 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
385 |
case False |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
386 |
hence "\<forall>i\<in>I. i < Suc(Max I)" |
38656 | 387 |
by (simp add: Max_less_iff [symmetric] finI) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
388 |
hence "\<forall>m \<ge> Suc(Max I). A m = {}" |
38656 | 389 |
by (simp add: I_def) (metis less_le_not_le) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
390 |
thus ?thesis |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
391 |
by blast |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
392 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
393 |
then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast |
38656 | 394 |
then have "\<forall>m\<ge>N. \<mu> (A m) = 0" by simp |
395 |
then have "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = setsum (\<lambda>m. \<mu> (A m)) {..<N}" |
|
396 |
by (simp add: psuminf_finite) |
|
397 |
also have "... = \<mu> (\<Union>i<N. A i)" |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
398 |
proof (induct N) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
399 |
case 0 thus ?case by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
400 |
next |
38656 | 401 |
case (Suc n) |
402 |
have "\<mu> (A n \<union> (\<Union> x<n. A x)) = \<mu> (A n) + \<mu> (\<Union> i<n. A i)" |
|
403 |
proof (rule Caratheodory.additiveD [OF add]) |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
404 |
show "A n \<inter> (\<Union> x<n. A x) = {}" using disj |
35582 | 405 |
by (auto simp add: disjoint_family_on_def nat_less_le) blast |
38656 | 406 |
show "A n \<in> sets M" using A |
407 |
by force |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
408 |
show "(\<Union>i<n. A i) \<in> sets M" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
409 |
proof (induct n) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
410 |
case 0 thus ?case by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
411 |
next |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
412 |
case (Suc n) thus ?case using A |
38656 | 413 |
by (simp add: lessThan_Suc Un range_subsetD) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
414 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
415 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
416 |
thus ?case using Suc |
38656 | 417 |
by (simp add: lessThan_Suc) |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
418 |
qed |
38656 | 419 |
also have "... = \<mu> (\<Union>i. A i)" |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
420 |
proof - |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
421 |
have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
422 |
by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE) |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
423 |
thus ?thesis by simp |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
424 |
qed |
38656 | 425 |
finally show "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" . |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
426 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
427 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset
|
428 |
|
35692 | 429 |
lemma (in measure_space) measure_setsum_split: |
430 |
assumes "finite r" and "a \<in> sets M" and br_in_M: "b ` r \<subseteq> sets M" |
|
431 |
assumes "(\<Union>i \<in> r. b i) = space M" |
|
432 |
assumes "disjoint_family_on b r" |
|
38656 | 433 |
shows "\<mu> a = (\<Sum> i \<in> r. \<mu> (a \<inter> (b i)))" |
35692 | 434 |
proof - |
38656 | 435 |
have *: "\<mu> a = \<mu> (\<Union>i \<in> r. a \<inter> b i)" |
35692 | 436 |
using assms by auto |
437 |
show ?thesis unfolding * |
|
438 |
proof (rule measure_finitely_additive''[symmetric]) |
|
439 |
show "finite r" using `finite r` by auto |
|
440 |
{ fix i assume "i \<in> r" |
|
441 |
hence "b i \<in> sets M" using br_in_M by auto |
|
442 |
thus "a \<inter> b i \<in> sets M" using `a \<in> sets M` by auto |
|
443 |
} |
|
444 |
show "disjoint_family_on (\<lambda>i. a \<inter> b i) r" |
|
445 |
using `disjoint_family_on b r` |
|
446 |
unfolding disjoint_family_on_def by auto |
|
447 |
qed |
|
448 |
qed |
|
449 |
||
38656 | 450 |
lemma (in measure_space) measure_subadditive: |
451 |
assumes measurable: "A \<in> sets M" "B \<in> sets M" |
|
452 |
shows "\<mu> (A \<union> B) \<le> \<mu> A + \<mu> B" |
|
453 |
proof - |
|
454 |
from measure_additive[of A "B - A"] |
|
455 |
have "\<mu> (A \<union> B) = \<mu> A + \<mu> (B - A)" |
|
456 |
using assms by (simp add: Diff) |
|
457 |
also have "\<dots> \<le> \<mu> A + \<mu> B" |
|
458 |
using assms by (auto intro!: add_left_mono measure_mono) |
|
459 |
finally show ?thesis . |
|
460 |
qed |
|
461 |
||
40859 | 462 |
lemma (in measure_space) measure_eq_0: |
463 |
assumes "N \<in> sets M" and "\<mu> N = 0" and "K \<subseteq> N" and "K \<in> sets M" |
|
464 |
shows "\<mu> K = 0" |
|
465 |
using measure_mono[OF assms(3,4,1)] assms(2) by auto |
|
466 |
||
39092 | 467 |
lemma (in measure_space) measure_finitely_subadditive: |
468 |
assumes "finite I" "A ` I \<subseteq> sets M" |
|
469 |
shows "\<mu> (\<Union>i\<in>I. A i) \<le> (\<Sum>i\<in>I. \<mu> (A i))" |
|
470 |
using assms proof induct |
|
471 |
case (insert i I) |
|
472 |
then have "(\<Union>i\<in>I. A i) \<in> sets M" by (auto intro: finite_UN) |
|
473 |
then have "\<mu> (\<Union>i\<in>insert i I. A i) \<le> \<mu> (A i) + \<mu> (\<Union>i\<in>I. A i)" |
|
474 |
using insert by (simp add: measure_subadditive) |
|
475 |
also have "\<dots> \<le> (\<Sum>i\<in>insert i I. \<mu> (A i))" |
|
476 |
using insert by (auto intro!: add_left_mono) |
|
477 |
finally show ?case . |
|
478 |
qed simp |
|
479 |
||
40859 | 480 |
lemma (in measure_space) measure_countably_subadditive: |
38656 | 481 |
assumes "range f \<subseteq> sets M" |
482 |
shows "\<mu> (\<Union>i. f i) \<le> (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))" |
|
483 |
proof - |
|
484 |
have "\<mu> (\<Union>i. f i) = \<mu> (\<Union>i. disjointed f i)" |
|
485 |
unfolding UN_disjointed_eq .. |
|
486 |
also have "\<dots> = (\<Sum>\<^isub>\<infinity> i. \<mu> (disjointed f i))" |
|
487 |
using range_disjointed_sets[OF assms] measure_countably_additive |
|
488 |
by (simp add: disjoint_family_disjointed comp_def) |
|
489 |
also have "\<dots> \<le> (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))" |
|
490 |
proof (rule psuminf_le, rule measure_mono) |
|
491 |
fix i show "disjointed f i \<subseteq> f i" by (rule disjointed_subset) |
|
492 |
show "f i \<in> sets M" "disjointed f i \<in> sets M" |
|
493 |
using assms range_disjointed_sets[OF assms] by auto |
|
494 |
qed |
|
495 |
finally show ?thesis . |
|
496 |
qed |
|
497 |
||
40859 | 498 |
lemma (in measure_space) measure_UN_eq_0: |
499 |
assumes "\<And> i :: nat. \<mu> (N i) = 0" and "range N \<subseteq> sets M" |
|
500 |
shows "\<mu> (\<Union> i. N i) = 0" |
|
501 |
using measure_countably_subadditive[OF assms(2)] assms(1) by auto |
|
502 |
||
39092 | 503 |
lemma (in measure_space) measure_inter_full_set: |
504 |
assumes "S \<in> sets M" "T \<in> sets M" and not_\<omega>: "\<mu> (T - S) \<noteq> \<omega>" |
|
505 |
assumes T: "\<mu> T = \<mu> (space M)" |
|
506 |
shows "\<mu> (S \<inter> T) = \<mu> S" |
|
507 |
proof (rule antisym) |
|
508 |
show " \<mu> (S \<inter> T) \<le> \<mu> S" |
|
509 |
using assms by (auto intro!: measure_mono) |
|
510 |
||
511 |
show "\<mu> S \<le> \<mu> (S \<inter> T)" |
|
512 |
proof (rule ccontr) |
|
513 |
assume contr: "\<not> ?thesis" |
|
514 |
have "\<mu> (space M) = \<mu> ((T - S) \<union> (S \<inter> T))" |
|
515 |
unfolding T[symmetric] by (auto intro!: arg_cong[where f="\<mu>"]) |
|
516 |
also have "\<dots> \<le> \<mu> (T - S) + \<mu> (S \<inter> T)" |
|
517 |
using assms by (auto intro!: measure_subadditive) |
|
518 |
also have "\<dots> < \<mu> (T - S) + \<mu> S" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
519 |
by (rule pextreal_less_add[OF not_\<omega>]) (insert contr, auto) |
39092 | 520 |
also have "\<dots> = \<mu> (T \<union> S)" |
521 |
using assms by (subst measure_additive) auto |
|
522 |
also have "\<dots> \<le> \<mu> (space M)" |
|
523 |
using assms sets_into_space by (auto intro!: measure_mono) |
|
524 |
finally show False .. |
|
525 |
qed |
|
526 |
qed |
|
527 |
||
40859 | 528 |
lemma measure_unique_Int_stable: |
529 |
fixes M E :: "'a algebra" and A :: "nat \<Rightarrow> 'a set" |
|
530 |
assumes "Int_stable E" "M = sigma E" |
|
531 |
and A: "range A \<subseteq> sets E" "A \<up> space E" |
|
532 |
and ms: "measure_space M \<mu>" "measure_space M \<nu>" |
|
533 |
and eq: "\<And>X. X \<in> sets E \<Longrightarrow> \<mu> X = \<nu> X" |
|
534 |
and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>" |
|
535 |
assumes "X \<in> sets M" |
|
536 |
shows "\<mu> X = \<nu> X" |
|
537 |
proof - |
|
538 |
let "?D F" = "{D. D \<in> sets M \<and> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)}" |
|
539 |
interpret M: measure_space M \<mu> by fact |
|
540 |
interpret M': measure_space M \<nu> by fact |
|
541 |
have "space E = space M" |
|
542 |
using `M = sigma E` by simp |
|
543 |
have sets_E: "sets E \<subseteq> Pow (space E)" |
|
544 |
proof |
|
545 |
fix X assume "X \<in> sets E" |
|
546 |
then have "X \<in> sets M" unfolding `M = sigma E` |
|
547 |
unfolding sigma_def by (auto intro!: sigma_sets.Basic) |
|
548 |
with M.sets_into_space show "X \<in> Pow (space E)" |
|
549 |
unfolding `space E = space M` by auto |
|
550 |
qed |
|
551 |
have A': "range A \<subseteq> sets M" using `M = sigma E` A |
|
552 |
by (auto simp: sets_sigma intro!: sigma_sets.Basic) |
|
553 |
{ fix F assume "F \<in> sets E" and "\<mu> F \<noteq> \<omega>" |
|
554 |
then have [intro]: "F \<in> sets M" unfolding `M = sigma E` sets_sigma |
|
555 |
by (intro sigma_sets.Basic) |
|
556 |
have "\<nu> F \<noteq> \<omega>" using `\<mu> F \<noteq> \<omega>` `F \<in> sets E` eq by simp |
|
557 |
interpret D: dynkin_system "\<lparr>space=space E, sets=?D F\<rparr>" |
|
558 |
proof (rule dynkin_systemI, simp_all) |
|
559 |
fix A assume "A \<in> sets M \<and> \<mu> (F \<inter> A) = \<nu> (F \<inter> A)" |
|
560 |
then show "A \<subseteq> space E" |
|
561 |
unfolding `space E = space M` using M.sets_into_space by auto |
|
562 |
next |
|
563 |
have "F \<inter> space E = F" using `F \<in> sets E` sets_E by auto |
|
564 |
then show "space E \<in> sets M \<and> \<mu> (F \<inter> space E) = \<nu> (F \<inter> space E)" |
|
565 |
unfolding `space E = space M` using `F \<in> sets E` eq by auto |
|
566 |
next |
|
567 |
fix A assume *: "A \<in> sets M \<and> \<mu> (F \<inter> A) = \<nu> (F \<inter> A)" |
|
568 |
then have **: "F \<inter> (space M - A) = F - (F \<inter> A)" |
|
569 |
and [intro]: "F \<inter> A \<in> sets M" |
|
570 |
using `F \<in> sets E` sets_E `space E = space M` by auto |
|
571 |
have "\<nu> (F \<inter> A) \<le> \<nu> F" by (auto intro!: M'.measure_mono) |
|
572 |
then have "\<nu> (F \<inter> A) \<noteq> \<omega>" using `\<nu> F \<noteq> \<omega>` by auto |
|
573 |
have "\<mu> (F \<inter> A) \<le> \<mu> F" by (auto intro!: M.measure_mono) |
|
574 |
then have "\<mu> (F \<inter> A) \<noteq> \<omega>" using `\<mu> F \<noteq> \<omega>` by auto |
|
575 |
then have "\<mu> (F \<inter> (space M - A)) = \<mu> F - \<mu> (F \<inter> A)" unfolding ** |
|
576 |
using `F \<inter> A \<in> sets M` by (auto intro!: M.measure_Diff) |
|
577 |
also have "\<dots> = \<nu> F - \<nu> (F \<inter> A)" using eq `F \<in> sets E` * by simp |
|
578 |
also have "\<dots> = \<nu> (F \<inter> (space M - A))" unfolding ** |
|
579 |
using `F \<inter> A \<in> sets M` `\<nu> (F \<inter> A) \<noteq> \<omega>` by (auto intro!: M'.measure_Diff[symmetric]) |
|
580 |
finally show "space E - A \<in> sets M \<and> \<mu> (F \<inter> (space E - A)) = \<nu> (F \<inter> (space E - A))" |
|
581 |
using `space E = space M` * by auto |
|
582 |
next |
|
583 |
fix A :: "nat \<Rightarrow> 'a set" |
|
584 |
assume "disjoint_family A" "range A \<subseteq> {X \<in> sets M. \<mu> (F \<inter> X) = \<nu> (F \<inter> X)}" |
|
585 |
then have A: "range (\<lambda>i. F \<inter> A i) \<subseteq> sets M" "F \<inter> (\<Union>x. A x) = (\<Union>x. F \<inter> A x)" |
|
586 |
"disjoint_family (\<lambda>i. F \<inter> A i)" "\<And>i. \<mu> (F \<inter> A i) = \<nu> (F \<inter> A i)" "range A \<subseteq> sets M" |
|
587 |
by ((fastsimp simp: disjoint_family_on_def)+) |
|
588 |
then show "(\<Union>x. A x) \<in> sets M \<and> \<mu> (F \<inter> (\<Union>x. A x)) = \<nu> (F \<inter> (\<Union>x. A x))" |
|
589 |
by (auto simp: M.measure_countably_additive[symmetric] |
|
590 |
M'.measure_countably_additive[symmetric] |
|
591 |
simp del: UN_simps) |
|
592 |
qed |
|
593 |
have *: "sigma E = \<lparr>space = space E, sets = ?D F\<rparr>" |
|
594 |
using `M = sigma E` `F \<in> sets E` `Int_stable E` |
|
595 |
by (intro D.dynkin_lemma) |
|
596 |
(auto simp add: sets_sigma Int_stable_def eq intro: sigma_sets.Basic) |
|
597 |
have "\<And>D. D \<in> sets M \<Longrightarrow> \<mu> (F \<inter> D) = \<nu> (F \<inter> D)" |
|
598 |
unfolding `M = sigma E` by (auto simp: *) } |
|
599 |
note * = this |
|
600 |
{ fix i have "\<mu> (A i \<inter> X) = \<nu> (A i \<inter> X)" |
|
601 |
using *[of "A i" X] `X \<in> sets M` A finite by auto } |
|
602 |
moreover |
|
603 |
have "(\<lambda>i. A i \<inter> X) \<up> X" |
|
604 |
using `X \<in> sets M` M.sets_into_space A `space E = space M` |
|
605 |
by (auto simp: isoton_def) |
|
606 |
then have "(\<lambda>i. \<mu> (A i \<inter> X)) \<up> \<mu> X" "(\<lambda>i. \<nu> (A i \<inter> X)) \<up> \<nu> X" |
|
607 |
using `X \<in> sets M` A' by (auto intro!: M.measure_up M'.measure_up M.Int) |
|
608 |
ultimately show ?thesis by (simp add: isoton_def) |
|
609 |
qed |
|
610 |
||
611 |
section "Isomorphisms between measure spaces" |
|
612 |
||
613 |
lemma (in measure_space) measure_space_isomorphic: |
|
614 |
fixes f :: "'c \<Rightarrow> 'a" |
|
615 |
assumes "bij_betw f S (space M)" |
|
616 |
shows "measure_space (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))" |
|
617 |
(is "measure_space ?T ?\<mu>") |
|
618 |
proof - |
|
619 |
have "f \<in> S \<rightarrow> space M" using assms unfolding bij_betw_def by auto |
|
620 |
then interpret T: sigma_algebra ?T by (rule sigma_algebra_vimage) |
|
621 |
show ?thesis |
|
622 |
proof |
|
623 |
show "\<mu> (f`{}) = 0" by simp |
|
624 |
show "countably_additive ?T (\<lambda>A. \<mu> (f ` A))" |
|
625 |
proof (unfold countably_additive_def, intro allI impI) |
|
626 |
fix A :: "nat \<Rightarrow> 'c set" assume "range A \<subseteq> sets ?T" "disjoint_family A" |
|
627 |
then have "\<forall>i. \<exists>F'. F' \<in> sets M \<and> A i = f -` F' \<inter> S" |
|
628 |
by (auto simp: image_iff image_subset_iff Bex_def vimage_algebra_def) |
|
629 |
from choice[OF this] obtain F where F: "\<And>i. F i \<in> sets M" and A: "\<And>i. A i = f -` F i \<inter> S" by auto |
|
630 |
then have [simp]: "\<And>i. f ` (A i) = F i" |
|
631 |
using sets_into_space assms |
|
632 |
by (force intro!: image_vimage_inter_eq[where T="space M"] simp: bij_betw_def) |
|
633 |
have "disjoint_family F" |
|
634 |
proof (intro disjoint_family_on_bisimulation[OF `disjoint_family A`]) |
|
635 |
fix n m assume "A n \<inter> A m = {}" |
|
636 |
then have "f -` (F n \<inter> F m) \<inter> S = {}" unfolding A by auto |
|
637 |
moreover |
|
638 |
have "F n \<in> sets M" "F m \<in> sets M" using F by auto |
|
639 |
then have "f`S = space M" "F n \<inter> F m \<subseteq> space M" |
|
640 |
using sets_into_space assms by (auto simp: bij_betw_def) |
|
641 |
note image_vimage_inter_eq[OF this, symmetric] |
|
642 |
ultimately show "F n \<inter> F m = {}" by simp |
|
643 |
qed |
|
644 |
with F show "(\<Sum>\<^isub>\<infinity> i. \<mu> (f ` A i)) = \<mu> (f ` (\<Union>i. A i))" |
|
645 |
by (auto simp add: image_UN intro!: measure_countably_additive) |
|
646 |
qed |
|
647 |
qed |
|
648 |
qed |
|
649 |
||
650 |
section "@{text \<mu>}-null sets" |
|
651 |
||
652 |
abbreviation (in measure_space) "null_sets \<equiv> {N\<in>sets M. \<mu> N = 0}" |
|
653 |
||
654 |
lemma (in measure_space) null_sets_Un[intro]: |
|
655 |
assumes "N \<in> null_sets" "N' \<in> null_sets" |
|
656 |
shows "N \<union> N' \<in> null_sets" |
|
657 |
proof (intro conjI CollectI) |
|
658 |
show "N \<union> N' \<in> sets M" using assms by auto |
|
659 |
have "\<mu> (N \<union> N') \<le> \<mu> N + \<mu> N'" |
|
660 |
using assms by (intro measure_subadditive) auto |
|
661 |
then show "\<mu> (N \<union> N') = 0" |
|
662 |
using assms by auto |
|
663 |
qed |
|
664 |
||
665 |
lemma UN_from_nat: "(\<Union>i. N i) = (\<Union>i. N (Countable.from_nat i))" |
|
666 |
proof - |
|
667 |
have "(\<Union>i. N i) = (\<Union>i. (N \<circ> Countable.from_nat) i)" |
|
668 |
unfolding SUPR_def image_compose |
|
669 |
unfolding surj_from_nat .. |
|
670 |
then show ?thesis by simp |
|
671 |
qed |
|
672 |
||
673 |
lemma (in measure_space) null_sets_UN[intro]: |
|
674 |
assumes "\<And>i::'i::countable. N i \<in> null_sets" |
|
675 |
shows "(\<Union>i. N i) \<in> null_sets" |
|
676 |
proof (intro conjI CollectI) |
|
677 |
show "(\<Union>i. N i) \<in> sets M" using assms by auto |
|
678 |
have "\<mu> (\<Union>i. N i) \<le> (\<Sum>\<^isub>\<infinity> n. \<mu> (N (Countable.from_nat n)))" |
|
679 |
unfolding UN_from_nat[of N] |
|
680 |
using assms by (intro measure_countably_subadditive) auto |
|
681 |
then show "\<mu> (\<Union>i. N i) = 0" |
|
682 |
using assms by auto |
|
683 |
qed |
|
684 |
||
40871 | 685 |
lemma (in measure_space) null_sets_finite_UN: |
686 |
assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets" |
|
687 |
shows "(\<Union>i\<in>S. A i) \<in> null_sets" |
|
688 |
proof (intro CollectI conjI) |
|
689 |
show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto |
|
690 |
have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))" |
|
691 |
using assms by (intro measure_finitely_subadditive) auto |
|
692 |
then show "\<mu> (\<Union>i\<in>S. A i) = 0" |
|
693 |
using assms by auto |
|
694 |
qed |
|
695 |
||
40859 | 696 |
lemma (in measure_space) null_set_Int1: |
697 |
assumes "B \<in> null_sets" "A \<in> sets M" shows "A \<inter> B \<in> null_sets" |
|
698 |
using assms proof (intro CollectI conjI) |
|
699 |
show "\<mu> (A \<inter> B) = 0" using assms by (intro measure_eq_0[of B "A \<inter> B"]) auto |
|
700 |
qed auto |
|
701 |
||
702 |
lemma (in measure_space) null_set_Int2: |
|
703 |
assumes "B \<in> null_sets" "A \<in> sets M" shows "B \<inter> A \<in> null_sets" |
|
704 |
using assms by (subst Int_commute) (rule null_set_Int1) |
|
705 |
||
706 |
lemma (in measure_space) measure_Diff_null_set: |
|
707 |
assumes "B \<in> null_sets" "A \<in> sets M" |
|
708 |
shows "\<mu> (A - B) = \<mu> A" |
|
709 |
proof - |
|
710 |
have *: "A - B = (A - (A \<inter> B))" by auto |
|
711 |
have "A \<inter> B \<in> null_sets" using assms by (rule null_set_Int1) |
|
712 |
then show ?thesis |
|
713 |
unfolding * using assms |
|
714 |
by (subst measure_Diff) auto |
|
715 |
qed |
|
716 |
||
717 |
lemma (in measure_space) null_set_Diff: |
|
718 |
assumes "B \<in> null_sets" "A \<in> sets M" shows "B - A \<in> null_sets" |
|
719 |
using assms proof (intro CollectI conjI) |
|
720 |
show "\<mu> (B - A) = 0" using assms by (intro measure_eq_0[of B "B - A"]) auto |
|
721 |
qed auto |
|
722 |
||
723 |
lemma (in measure_space) measure_Un_null_set: |
|
724 |
assumes "A \<in> sets M" "B \<in> null_sets" |
|
725 |
shows "\<mu> (A \<union> B) = \<mu> A" |
|
726 |
proof - |
|
727 |
have *: "A \<union> B = A \<union> (B - A)" by auto |
|
728 |
have "B - A \<in> null_sets" using assms(2,1) by (rule null_set_Diff) |
|
729 |
then show ?thesis |
|
730 |
unfolding * using assms |
|
731 |
by (subst measure_additive[symmetric]) auto |
|
732 |
qed |
|
733 |
||
40871 | 734 |
section "Formalise almost everywhere" |
735 |
||
736 |
definition (in measure_space) |
|
737 |
almost_everywhere :: "('a \<Rightarrow> bool) \<Rightarrow> bool" (binder "AE " 10) where |
|
738 |
"almost_everywhere P \<longleftrightarrow> (\<exists>N\<in>null_sets. { x \<in> space M. \<not> P x } \<subseteq> N)" |
|
739 |
||
740 |
lemma (in measure_space) AE_I': |
|
741 |
"N \<in> null_sets \<Longrightarrow> {x\<in>space M. \<not> P x} \<subseteq> N \<Longrightarrow> (AE x. P x)" |
|
742 |
unfolding almost_everywhere_def by auto |
|
743 |
||
744 |
lemma (in measure_space) AE_iff_null_set: |
|
745 |
assumes "{x\<in>space M. \<not> P x} \<in> sets M" (is "?P \<in> sets M") |
|
746 |
shows "(AE x. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets" |
|
747 |
proof |
|
748 |
assume "AE x. P x" then obtain N where N: "N \<in> sets M" "?P \<subseteq> N" "\<mu> N = 0" |
|
749 |
unfolding almost_everywhere_def by auto |
|
750 |
moreover have "\<mu> ?P \<le> \<mu> N" |
|
751 |
using assms N(1,2) by (auto intro: measure_mono) |
|
752 |
ultimately show "?P \<in> null_sets" using assms by auto |
|
753 |
next |
|
754 |
assume "?P \<in> null_sets" with assms show "AE x. P x" by (auto intro: AE_I') |
|
755 |
qed |
|
756 |
||
40859 | 757 |
lemma (in measure_space) AE_True[intro, simp]: "AE x. True" |
758 |
unfolding almost_everywhere_def by auto |
|
759 |
||
760 |
lemma (in measure_space) AE_E[consumes 1]: |
|
761 |
assumes "AE x. P x" |
|
762 |
obtains N where "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M" |
|
763 |
using assms unfolding almost_everywhere_def by auto |
|
764 |
||
765 |
lemma (in measure_space) AE_I: |
|
766 |
assumes "{x \<in> space M. \<not> P x} \<subseteq> N" "\<mu> N = 0" "N \<in> sets M" |
|
767 |
shows "AE x. P x" |
|
768 |
using assms unfolding almost_everywhere_def by auto |
|
769 |
||
770 |
lemma (in measure_space) AE_mp: |
|
771 |
assumes AE_P: "AE x. P x" and AE_imp: "AE x. P x \<longrightarrow> Q x" |
|
772 |
shows "AE x. Q x" |
|
773 |
proof - |
|
774 |
from AE_P obtain A where P: "{x\<in>space M. \<not> P x} \<subseteq> A" |
|
775 |
and A: "A \<in> sets M" "\<mu> A = 0" |
|
776 |
by (auto elim!: AE_E) |
|
777 |
||
778 |
from AE_imp obtain B where imp: "{x\<in>space M. P x \<and> \<not> Q x} \<subseteq> B" |
|
779 |
and B: "B \<in> sets M" "\<mu> B = 0" |
|
780 |
by (auto elim!: AE_E) |
|
781 |
||
782 |
show ?thesis |
|
783 |
proof (intro AE_I) |
|
784 |
show "A \<union> B \<in> sets M" "\<mu> (A \<union> B) = 0" using A B |
|
785 |
using measure_subadditive[of A B] by auto |
|
786 |
show "{x\<in>space M. \<not> Q x} \<subseteq> A \<union> B" |
|
787 |
using P imp by auto |
|
788 |
qed |
|
789 |
qed |
|
790 |
||
791 |
lemma (in measure_space) AE_iffI: |
|
792 |
assumes P: "AE x. P x" and Q: "AE x. P x \<longleftrightarrow> Q x" shows "AE x. Q x" |
|
793 |
using AE_mp[OF Q, of "\<lambda>x. P x \<longrightarrow> Q x"] AE_mp[OF P, of Q] by auto |
|
794 |
||
795 |
lemma (in measure_space) AE_disjI1: |
|
796 |
assumes P: "AE x. P x" shows "AE x. P x \<or> Q x" |
|
797 |
by (rule AE_mp[OF P]) auto |
|
798 |
||
799 |
lemma (in measure_space) AE_disjI2: |
|
800 |
assumes P: "AE x. Q x" shows "AE x. P x \<or> Q x" |
|
801 |
by (rule AE_mp[OF P]) auto |
|
802 |
||
803 |
lemma (in measure_space) AE_conjI: |
|
804 |
assumes AE_P: "AE x. P x" and AE_Q: "AE x. Q x" |
|
805 |
shows "AE x. P x \<and> Q x" |
|
41660 | 806 |
apply (rule AE_mp[OF AE_P]) |
807 |
apply (rule AE_mp[OF AE_Q]) |
|
808 |
by simp |
|
40859 | 809 |
|
41660 | 810 |
lemma (in measure_space) AE_conj_iff[simp]: |
811 |
shows "(AE x. P x \<and> Q x) \<longleftrightarrow> (AE x. P x) \<and> (AE x. Q x)" |
|
812 |
proof (intro conjI iffI AE_conjI) |
|
813 |
assume *: "AE x. P x \<and> Q x" |
|
814 |
from * show "AE x. P x" by (rule AE_mp) auto |
|
815 |
from * show "AE x. Q x" by (rule AE_mp) auto |
|
816 |
qed auto |
|
40859 | 817 |
|
818 |
lemma (in measure_space) AE_E2: |
|
819 |
assumes "AE x. P x" "{x\<in>space M. P x} \<in> sets M" |
|
820 |
shows "\<mu> {x\<in>space M. \<not> P x} = 0" (is "\<mu> ?P = 0") |
|
821 |
proof - |
|
822 |
obtain A where A: "?P \<subseteq> A" "A \<in> sets M" "\<mu> A = 0" |
|
823 |
using assms by (auto elim!: AE_E) |
|
824 |
have "?P = space M - {x\<in>space M. P x}" by auto |
|
825 |
then have "?P \<in> sets M" using assms by auto |
|
826 |
with assms `?P \<subseteq> A` `A \<in> sets M` have "\<mu> ?P \<le> \<mu> A" |
|
827 |
by (auto intro!: measure_mono) |
|
828 |
then show "\<mu> ?P = 0" using A by simp |
|
829 |
qed |
|
830 |
||
831 |
lemma (in measure_space) AE_space[simp, intro]: "AE x. x \<in> space M" |
|
832 |
by (rule AE_I[where N="{}"]) auto |
|
833 |
||
834 |
lemma (in measure_space) AE_cong: |
|
835 |
assumes "\<And>x. x \<in> space M \<Longrightarrow> P x" shows "AE x. P x" |
|
836 |
proof - |
|
837 |
have [simp]: "\<And>x. (x \<in> space M \<longrightarrow> P x) \<longleftrightarrow> True" using assms by auto |
|
838 |
show ?thesis |
|
839 |
by (rule AE_mp[OF AE_space]) auto |
|
840 |
qed |
|
841 |
||
842 |
lemma (in measure_space) all_AE_countable: |
|
843 |
"(\<forall>i::'i::countable. AE x. P i x) \<longleftrightarrow> (AE x. \<forall>i. P i x)" |
|
844 |
proof |
|
845 |
assume "\<forall>i. AE x. P i x" |
|
846 |
from this[unfolded almost_everywhere_def Bex_def, THEN choice] |
|
847 |
obtain N where N: "\<And>i. N i \<in> null_sets" "\<And>i. {x\<in>space M. \<not> P i x} \<subseteq> N i" by auto |
|
848 |
have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. {x\<in>space M. \<not> P i x})" by auto |
|
849 |
also have "\<dots> \<subseteq> (\<Union>i. N i)" using N by auto |
|
850 |
finally have "{x\<in>space M. \<not> (\<forall>i. P i x)} \<subseteq> (\<Union>i. N i)" . |
|
851 |
moreover from N have "(\<Union>i. N i) \<in> null_sets" |
|
852 |
by (intro null_sets_UN) auto |
|
853 |
ultimately show "AE x. \<forall>i. P i x" |
|
854 |
unfolding almost_everywhere_def by auto |
|
855 |
next |
|
856 |
assume *: "AE x. \<forall>i. P i x" |
|
857 |
show "\<forall>i. AE x. P i x" |
|
858 |
by (rule allI, rule AE_mp[OF *]) simp |
|
859 |
qed |
|
860 |
||
38656 | 861 |
lemma (in measure_space) restricted_measure_space: |
862 |
assumes "S \<in> sets M" |
|
39092 | 863 |
shows "measure_space (restricted_space S) \<mu>" |
38656 | 864 |
(is "measure_space ?r \<mu>") |
865 |
unfolding measure_space_def measure_space_axioms_def |
|
866 |
proof safe |
|
867 |
show "sigma_algebra ?r" using restricted_sigma_algebra[OF assms] . |
|
868 |
show "\<mu> {} = 0" by simp |
|
869 |
show "countably_additive ?r \<mu>" |
|
870 |
unfolding countably_additive_def |
|
871 |
proof safe |
|
872 |
fix A :: "nat \<Rightarrow> 'a set" |
|
873 |
assume *: "range A \<subseteq> sets ?r" and **: "disjoint_family A" |
|
874 |
from restriction_in_sets[OF assms *[simplified]] ** |
|
875 |
show "(\<Sum>\<^isub>\<infinity> n. \<mu> (A n)) = \<mu> (\<Union>i. A i)" |
|
876 |
using measure_countably_additive by simp |
|
877 |
qed |
|
878 |
qed |
|
879 |
||
39089 | 880 |
lemma (in measure_space) measure_space_vimage: |
40859 | 881 |
fixes M' :: "'b algebra" |
39089 | 882 |
assumes "f \<in> measurable M M'" |
883 |
and "sigma_algebra M'" |
|
884 |
shows "measure_space M' (\<lambda>A. \<mu> (f -` A \<inter> space M))" (is "measure_space M' ?T") |
|
885 |
proof - |
|
886 |
interpret M': sigma_algebra M' by fact |
|
887 |
||
888 |
show ?thesis |
|
889 |
proof |
|
890 |
show "?T {} = 0" by simp |
|
891 |
||
892 |
show "countably_additive M' ?T" |
|
893 |
proof (unfold countably_additive_def, safe) |
|
40859 | 894 |
fix A :: "nat \<Rightarrow> 'b set" assume "range A \<subseteq> sets M'" "disjoint_family A" |
39089 | 895 |
hence *: "\<And>i. f -` (A i) \<inter> space M \<in> sets M" |
896 |
using `f \<in> measurable M M'` by (auto simp: measurable_def) |
|
897 |
moreover have "(\<Union>i. f -` A i \<inter> space M) \<in> sets M" |
|
898 |
using * by blast |
|
899 |
moreover have **: "disjoint_family (\<lambda>i. f -` A i \<inter> space M)" |
|
900 |
using `disjoint_family A` by (auto simp: disjoint_family_on_def) |
|
901 |
ultimately show "(\<Sum>\<^isub>\<infinity> i. ?T (A i)) = ?T (\<Union>i. A i)" |
|
902 |
using measure_countably_additive[OF _ **] by (auto simp: comp_def vimage_UN) |
|
903 |
qed |
|
904 |
qed |
|
905 |
qed |
|
906 |
||
39092 | 907 |
lemma (in measure_space) measure_space_subalgebra: |
41545 | 908 |
assumes "sigma_algebra N" and [simp]: "sets N \<subseteq> sets M" "space N = space M" |
909 |
shows "measure_space N \<mu>" |
|
39092 | 910 |
proof - |
41545 | 911 |
interpret N: sigma_algebra N by fact |
39092 | 912 |
show ?thesis |
913 |
proof |
|
41545 | 914 |
from `sets N \<subseteq> sets M` have "\<And>A. range A \<subseteq> sets N \<Longrightarrow> range A \<subseteq> sets M" by blast |
915 |
then show "countably_additive N \<mu>" |
|
916 |
by (auto intro!: measure_countably_additive simp: countably_additive_def) |
|
39092 | 917 |
qed simp |
918 |
qed |
|
919 |
||
38656 | 920 |
section "@{text \<sigma>}-finite Measures" |
921 |
||
922 |
locale sigma_finite_measure = measure_space + |
|
923 |
assumes sigma_finite: "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)" |
|
924 |
||
925 |
lemma (in sigma_finite_measure) restricted_sigma_finite_measure: |
|
926 |
assumes "S \<in> sets M" |
|
39092 | 927 |
shows "sigma_finite_measure (restricted_space S) \<mu>" |
38656 | 928 |
(is "sigma_finite_measure ?r _") |
929 |
unfolding sigma_finite_measure_def sigma_finite_measure_axioms_def |
|
930 |
proof safe |
|
931 |
show "measure_space ?r \<mu>" using restricted_measure_space[OF assms] . |
|
932 |
next |
|
933 |
obtain A :: "nat \<Rightarrow> 'a set" where |
|
934 |
"range A \<subseteq> sets M" "(\<Union>i. A i) = space M" "\<And>i. \<mu> (A i) \<noteq> \<omega>" |
|
935 |
using sigma_finite by auto |
|
936 |
show "\<exists>A::nat \<Rightarrow> 'a set. range A \<subseteq> sets ?r \<and> (\<Union>i. A i) = space ?r \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)" |
|
937 |
proof (safe intro!: exI[of _ "\<lambda>i. A i \<inter> S"] del: notI) |
|
938 |
fix i |
|
939 |
show "A i \<inter> S \<in> sets ?r" |
|
940 |
using `range A \<subseteq> sets M` `S \<in> sets M` by auto |
|
941 |
next |
|
942 |
fix x i assume "x \<in> S" thus "x \<in> space ?r" by simp |
|
943 |
next |
|
944 |
fix x assume "x \<in> space ?r" thus "x \<in> (\<Union>i. A i \<inter> S)" |
|
945 |
using `(\<Union>i. A i) = space M` `S \<in> sets M` by auto |
|
946 |
next |
|
947 |
fix i |
|
948 |
have "\<mu> (A i \<inter> S) \<le> \<mu> (A i)" |
|
949 |
using `range A \<subseteq> sets M` `S \<in> sets M` by (auto intro!: measure_mono) |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
950 |
also have "\<dots> < \<omega>" using `\<mu> (A i) \<noteq> \<omega>` by (auto simp: pextreal_less_\<omega>) |
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
951 |
finally show "\<mu> (A i \<inter> S) \<noteq> \<omega>" by (auto simp: pextreal_less_\<omega>) |
38656 | 952 |
qed |
953 |
qed |
|
954 |
||
40859 | 955 |
lemma (in sigma_finite_measure) sigma_finite_measure_cong: |
956 |
assumes cong: "\<And>A. A \<in> sets M \<Longrightarrow> \<mu>' A = \<mu> A" |
|
957 |
shows "sigma_finite_measure M \<mu>'" |
|
958 |
proof - |
|
959 |
interpret \<mu>': measure_space M \<mu>' |
|
960 |
using cong by (rule measure_space_cong) |
|
961 |
from sigma_finite guess A .. note A = this |
|
962 |
then have "\<And>i. A i \<in> sets M" by auto |
|
963 |
with A have fin: "(\<forall>i. \<mu>' (A i) \<noteq> \<omega>)" using cong by auto |
|
964 |
show ?thesis |
|
965 |
apply default |
|
966 |
using A fin by auto |
|
967 |
qed |
|
968 |
||
39092 | 969 |
lemma (in sigma_finite_measure) disjoint_sigma_finite: |
970 |
"\<exists>A::nat\<Rightarrow>'a set. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> |
|
971 |
(\<forall>i. \<mu> (A i) \<noteq> \<omega>) \<and> disjoint_family A" |
|
972 |
proof - |
|
973 |
obtain A :: "nat \<Rightarrow> 'a set" where |
|
974 |
range: "range A \<subseteq> sets M" and |
|
975 |
space: "(\<Union>i. A i) = space M" and |
|
976 |
measure: "\<And>i. \<mu> (A i) \<noteq> \<omega>" |
|
977 |
using sigma_finite by auto |
|
978 |
note range' = range_disjointed_sets[OF range] range |
|
979 |
{ fix i |
|
980 |
have "\<mu> (disjointed A i) \<le> \<mu> (A i)" |
|
981 |
using range' disjointed_subset[of A i] by (auto intro!: measure_mono) |
|
982 |
then have "\<mu> (disjointed A i) \<noteq> \<omega>" |
|
983 |
using measure[of i] by auto } |
|
984 |
with disjoint_family_disjointed UN_disjointed_eq[of A] space range' |
|
985 |
show ?thesis by (auto intro!: exI[of _ "disjointed A"]) |
|
986 |
qed |
|
987 |
||
40859 | 988 |
lemma (in sigma_finite_measure) sigma_finite_up: |
989 |
"\<exists>F. range F \<subseteq> sets M \<and> F \<up> space M \<and> (\<forall>i. \<mu> (F i) \<noteq> \<omega>)" |
|
990 |
proof - |
|
991 |
obtain F :: "nat \<Rightarrow> 'a set" where |
|
992 |
F: "range F \<subseteq> sets M" "(\<Union>i. F i) = space M" "\<And>i. \<mu> (F i) \<noteq> \<omega>" |
|
993 |
using sigma_finite by auto |
|
994 |
then show ?thesis unfolding isoton_def |
|
995 |
proof (intro exI[of _ "\<lambda>n. \<Union>i\<le>n. F i"] conjI allI) |
|
996 |
from F have "\<And>x. x \<in> space M \<Longrightarrow> \<exists>i. x \<in> F i" by auto |
|
997 |
then show "(\<Union>n. \<Union> i\<le>n. F i) = space M" |
|
998 |
using F by fastsimp |
|
999 |
next |
|
1000 |
fix n |
|
1001 |
have "\<mu> (\<Union> i\<le>n. F i) \<le> (\<Sum>i\<le>n. \<mu> (F i))" using F |
|
1002 |
by (auto intro!: measure_finitely_subadditive) |
|
1003 |
also have "\<dots> < \<omega>" |
|
1004 |
using F by (auto simp: setsum_\<omega>) |
|
1005 |
finally show "\<mu> (\<Union> i\<le>n. F i) \<noteq> \<omega>" by simp |
|
1006 |
qed force+ |
|
1007 |
qed |
|
1008 |
||
1009 |
lemma (in sigma_finite_measure) sigma_finite_measure_isomorphic: |
|
1010 |
assumes f: "bij_betw f S (space M)" |
|
1011 |
shows "sigma_finite_measure (vimage_algebra S f) (\<lambda>A. \<mu> (f ` A))" |
|
1012 |
proof - |
|
1013 |
interpret M: measure_space "vimage_algebra S f" "\<lambda>A. \<mu> (f ` A)" |
|
1014 |
using f by (rule measure_space_isomorphic) |
|
1015 |
show ?thesis |
|
1016 |
proof default |
|
1017 |
from sigma_finite guess A::"nat \<Rightarrow> 'a set" .. note A = this |
|
1018 |
show "\<exists>A::nat\<Rightarrow>'b set. range A \<subseteq> sets (vimage_algebra S f) \<and> (\<Union>i. A i) = space (vimage_algebra S f) \<and> (\<forall>i. \<mu> (f ` A i) \<noteq> \<omega>)" |
|
1019 |
proof (intro exI conjI) |
|
1020 |
show "(\<Union>i::nat. f -` A i \<inter> S) = space (vimage_algebra S f)" |
|
1021 |
using A f[THEN bij_betw_imp_funcset] by (auto simp: vimage_UN[symmetric]) |
|
1022 |
show "range (\<lambda>i. f -` A i \<inter> S) \<subseteq> sets (vimage_algebra S f)" |
|
1023 |
using A by (auto simp: vimage_algebra_def) |
|
1024 |
have "\<And>i. f ` (f -` A i \<inter> S) = A i" |
|
1025 |
using f A sets_into_space |
|
1026 |
by (intro image_vimage_inter_eq) (auto simp: bij_betw_def) |
|
1027 |
then show "\<forall>i. \<mu> (f ` (f -` A i \<inter> S)) \<noteq> \<omega>" using A by simp |
|
1028 |
qed |
|
1029 |
qed |
|
1030 |
qed |
|
1031 |
||
38656 | 1032 |
section "Real measure values" |
1033 |
||
1034 |
lemma (in measure_space) real_measure_Union: |
|
1035 |
assumes finite: "\<mu> A \<noteq> \<omega>" "\<mu> B \<noteq> \<omega>" |
|
1036 |
and measurable: "A \<in> sets M" "B \<in> sets M" "A \<inter> B = {}" |
|
1037 |
shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)" |
|
1038 |
unfolding measure_additive[symmetric, OF measurable] |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1039 |
using finite by (auto simp: real_of_pextreal_add) |
38656 | 1040 |
|
1041 |
lemma (in measure_space) real_measure_finite_Union: |
|
1042 |
assumes measurable: |
|
1043 |
"finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M" "disjoint_family_on A S" |
|
1044 |
assumes finite: "\<And>i. i \<in> S \<Longrightarrow> \<mu> (A i) \<noteq> \<omega>" |
|
1045 |
shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1046 |
using real_of_pextreal_setsum[of S, OF finite] |
38656 | 1047 |
measure_finitely_additive''[symmetric, OF measurable] |
1048 |
by simp |
|
1049 |
||
1050 |
lemma (in measure_space) real_measure_Diff: |
|
1051 |
assumes finite: "\<mu> A \<noteq> \<omega>" |
|
1052 |
and measurable: "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A" |
|
1053 |
shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)" |
|
1054 |
proof - |
|
1055 |
have "\<mu> (A - B) \<le> \<mu> A" |
|
1056 |
"\<mu> B \<le> \<mu> A" |
|
1057 |
using measurable by (auto intro!: measure_mono) |
|
1058 |
hence "real (\<mu> ((A - B) \<union> B)) = real (\<mu> (A - B)) + real (\<mu> B)" |
|
1059 |
using measurable finite by (rule_tac real_measure_Union) auto |
|
1060 |
thus ?thesis using `B \<subseteq> A` by (auto simp: Un_absorb2) |
|
1061 |
qed |
|
1062 |
||
1063 |
lemma (in measure_space) real_measure_UNION: |
|
1064 |
assumes measurable: "range A \<subseteq> sets M" "disjoint_family A" |
|
1065 |
assumes finite: "\<mu> (\<Union>i. A i) \<noteq> \<omega>" |
|
1066 |
shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))" |
|
1067 |
proof - |
|
1068 |
have *: "(\<Sum>\<^isub>\<infinity> i. \<mu> (A i)) = \<mu> (\<Union>i. A i)" |
|
1069 |
using measure_countably_additive[OF measurable] by (simp add: comp_def) |
|
1070 |
hence "(\<Sum>\<^isub>\<infinity> i. \<mu> (A i)) \<noteq> \<omega>" using finite by simp |
|
1071 |
from psuminf_imp_suminf[OF this] |
|
1072 |
show ?thesis using * by simp |
|
1073 |
qed |
|
1074 |
||
1075 |
lemma (in measure_space) real_measure_subadditive: |
|
1076 |
assumes measurable: "A \<in> sets M" "B \<in> sets M" |
|
1077 |
and fin: "\<mu> A \<noteq> \<omega>" "\<mu> B \<noteq> \<omega>" |
|
1078 |
shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)" |
|
1079 |
proof - |
|
1080 |
have "real (\<mu> (A \<union> B)) \<le> real (\<mu> A + \<mu> B)" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1081 |
using measure_subadditive[OF measurable] fin by (auto intro!: real_of_pextreal_mono) |
38656 | 1082 |
also have "\<dots> = real (\<mu> A) + real (\<mu> B)" |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1083 |
using fin by (simp add: real_of_pextreal_add) |
38656 | 1084 |
finally show ?thesis . |
1085 |
qed |
|
1086 |
||
40859 | 1087 |
lemma (in measure_space) real_measure_countably_subadditive: |
38656 | 1088 |
assumes "range f \<subseteq> sets M" and "(\<Sum>\<^isub>\<infinity> i. \<mu> (f i)) \<noteq> \<omega>" |
1089 |
shows "real (\<mu> (\<Union>i. f i)) \<le> (\<Sum> i. real (\<mu> (f i)))" |
|
1090 |
proof - |
|
1091 |
have "real (\<mu> (\<Union>i. f i)) \<le> real (\<Sum>\<^isub>\<infinity> i. \<mu> (f i))" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1092 |
using assms by (auto intro!: real_of_pextreal_mono measure_countably_subadditive) |
38656 | 1093 |
also have "\<dots> = (\<Sum> i. real (\<mu> (f i)))" |
1094 |
using assms by (auto intro!: sums_unique psuminf_imp_suminf) |
|
1095 |
finally show ?thesis . |
|
1096 |
qed |
|
1097 |
||
1098 |
lemma (in measure_space) real_measure_setsum_singleton: |
|
1099 |
assumes S: "finite S" "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M" |
|
1100 |
and fin: "\<And>x. x \<in> S \<Longrightarrow> \<mu> {x} \<noteq> \<omega>" |
|
1101 |
shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1102 |
using measure_finite_singleton[OF S] fin by (simp add: real_of_pextreal_setsum) |
38656 | 1103 |
|
1104 |
lemma (in measure_space) real_continuity_from_below: |
|
1105 |
assumes A: "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)" and "\<mu> (\<Union>i. A i) \<noteq> \<omega>" |
|
1106 |
shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))" |
|
1107 |
proof (rule SUP_eq_LIMSEQ[THEN iffD1]) |
|
1108 |
{ fix n have "\<mu> (A n) \<le> \<mu> (\<Union>i. A i)" |
|
1109 |
using A by (auto intro!: measure_mono) |
|
1110 |
hence "\<mu> (A n) \<noteq> \<omega>" using assms by auto } |
|
1111 |
note this[simp] |
|
1112 |
||
1113 |
show "mono (\<lambda>i. real (\<mu> (A i)))" unfolding mono_iff_le_Suc using A |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1114 |
by (auto intro!: real_of_pextreal_mono measure_mono) |
38656 | 1115 |
|
1116 |
show "(SUP n. Real (real (\<mu> (A n)))) = Real (real (\<mu> (\<Union>i. A i)))" |
|
1117 |
using continuity_from_below[OF A(1), OF A(2)] |
|
1118 |
using assms by (simp add: Real_real) |
|
1119 |
qed simp_all |
|
1120 |
||
1121 |
lemma (in measure_space) real_continuity_from_above: |
|
1122 |
assumes A: "range A \<subseteq> sets M" |
|
1123 |
and mono_Suc: "\<And>n. A (Suc n) \<subseteq> A n" |
|
1124 |
and finite: "\<And>i. \<mu> (A i) \<noteq> \<omega>" |
|
1125 |
shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))" |
|
1126 |
proof (rule INF_eq_LIMSEQ[THEN iffD1]) |
|
1127 |
{ fix n have "\<mu> (\<Inter>i. A i) \<le> \<mu> (A n)" |
|
1128 |
using A by (auto intro!: measure_mono) |
|
1129 |
hence "\<mu> (\<Inter>i. A i) \<noteq> \<omega>" using assms by auto } |
|
1130 |
note this[simp] |
|
1131 |
||
1132 |
show "mono (\<lambda>i. - real (\<mu> (A i)))" unfolding mono_iff_le_Suc using assms |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1133 |
by (auto intro!: real_of_pextreal_mono measure_mono) |
38656 | 1134 |
|
1135 |
show "(INF n. Real (real (\<mu> (A n)))) = |
|
1136 |
Real (real (\<mu> (\<Inter>i. A i)))" |
|
1137 |
using continuity_from_above[OF A, OF mono_Suc finite] |
|
1138 |
using assms by (simp add: Real_real) |
|
1139 |
qed simp_all |
|
1140 |
||
1141 |
locale finite_measure = measure_space + |
|
1142 |
assumes finite_measure_of_space: "\<mu> (space M) \<noteq> \<omega>" |
|
1143 |
||
1144 |
sublocale finite_measure < sigma_finite_measure |
|
1145 |
proof |
|
1146 |
show "\<exists>A. range A \<subseteq> sets M \<and> (\<Union>i. A i) = space M \<and> (\<forall>i. \<mu> (A i) \<noteq> \<omega>)" |
|
1147 |
using finite_measure_of_space by (auto intro!: exI[of _ "\<lambda>x. space M"]) |
|
1148 |
qed |
|
1149 |
||
39092 | 1150 |
lemma (in finite_measure) finite_measure[simp, intro]: |
38656 | 1151 |
assumes "A \<in> sets M" |
1152 |
shows "\<mu> A \<noteq> \<omega>" |
|
1153 |
proof - |
|
1154 |
from `A \<in> sets M` have "A \<subseteq> space M" |
|
1155 |
using sets_into_space by blast |
|
1156 |
hence "\<mu> A \<le> \<mu> (space M)" |
|
1157 |
using assms top by (rule measure_mono) |
|
1158 |
also have "\<dots> < \<omega>" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1159 |
using finite_measure_of_space unfolding pextreal_less_\<omega> . |
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1160 |
finally show ?thesis unfolding pextreal_less_\<omega> . |
38656 | 1161 |
qed |
1162 |
||
1163 |
lemma (in finite_measure) restricted_finite_measure: |
|
1164 |
assumes "S \<in> sets M" |
|
39092 | 1165 |
shows "finite_measure (restricted_space S) \<mu>" |
38656 | 1166 |
(is "finite_measure ?r _") |
1167 |
unfolding finite_measure_def finite_measure_axioms_def |
|
1168 |
proof (safe del: notI) |
|
1169 |
show "measure_space ?r \<mu>" using restricted_measure_space[OF assms] . |
|
1170 |
next |
|
1171 |
show "\<mu> (space ?r) \<noteq> \<omega>" using finite_measure[OF `S \<in> sets M`] by auto |
|
1172 |
qed |
|
1173 |
||
40859 | 1174 |
lemma (in measure_space) restricted_to_finite_measure: |
1175 |
assumes "S \<in> sets M" "\<mu> S \<noteq> \<omega>" |
|
1176 |
shows "finite_measure (restricted_space S) \<mu>" |
|
1177 |
proof - |
|
1178 |
have "measure_space (restricted_space S) \<mu>" |
|
1179 |
using `S \<in> sets M` by (rule restricted_measure_space) |
|
1180 |
then show ?thesis |
|
1181 |
unfolding finite_measure_def finite_measure_axioms_def |
|
1182 |
using assms by auto |
|
1183 |
qed |
|
1184 |
||
38656 | 1185 |
lemma (in finite_measure) real_finite_measure_Diff: |
1186 |
assumes "A \<in> sets M" "B \<in> sets M" "B \<subseteq> A" |
|
1187 |
shows "real (\<mu> (A - B)) = real (\<mu> A) - real (\<mu> B)" |
|
1188 |
using finite_measure[OF `A \<in> sets M`] by (rule real_measure_Diff[OF _ assms]) |
|
1189 |
||
1190 |
lemma (in finite_measure) real_finite_measure_Union: |
|
1191 |
assumes sets: "A \<in> sets M" "B \<in> sets M" and "A \<inter> B = {}" |
|
1192 |
shows "real (\<mu> (A \<union> B)) = real (\<mu> A) + real (\<mu> B)" |
|
1193 |
using sets by (auto intro!: real_measure_Union[OF _ _ assms] finite_measure) |
|
1194 |
||
1195 |
lemma (in finite_measure) real_finite_measure_finite_Union: |
|
1196 |
assumes "finite S" and dis: "disjoint_family_on A S" |
|
1197 |
and *: "\<And>i. i \<in> S \<Longrightarrow> A i \<in> sets M" |
|
1198 |
shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))" |
|
1199 |
proof (rule real_measure_finite_Union[OF `finite S` _ dis]) |
|
1200 |
fix i assume "i \<in> S" from *[OF this] show "A i \<in> sets M" . |
|
1201 |
from finite_measure[OF this] show "\<mu> (A i) \<noteq> \<omega>" . |
|
1202 |
qed |
|
1203 |
||
1204 |
lemma (in finite_measure) real_finite_measure_UNION: |
|
1205 |
assumes measurable: "range A \<subseteq> sets M" "disjoint_family A" |
|
1206 |
shows "(\<lambda>i. real (\<mu> (A i))) sums (real (\<mu> (\<Union>i. A i)))" |
|
1207 |
proof (rule real_measure_UNION[OF assms]) |
|
1208 |
have "(\<Union>i. A i) \<in> sets M" using measurable(1) by (rule countable_UN) |
|
1209 |
thus "\<mu> (\<Union>i. A i) \<noteq> \<omega>" by (rule finite_measure) |
|
1210 |
qed |
|
1211 |
||
1212 |
lemma (in finite_measure) real_measure_mono: |
|
1213 |
"A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A \<subseteq> B \<Longrightarrow> real (\<mu> A) \<le> real (\<mu> B)" |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1214 |
by (auto intro!: measure_mono real_of_pextreal_mono finite_measure) |
38656 | 1215 |
|
1216 |
lemma (in finite_measure) real_finite_measure_subadditive: |
|
1217 |
assumes measurable: "A \<in> sets M" "B \<in> sets M" |
|
1218 |
shows "real (\<mu> (A \<union> B)) \<le> real (\<mu> A) + real (\<mu> B)" |
|
1219 |
using measurable measurable[THEN finite_measure] by (rule real_measure_subadditive) |
|
1220 |
||
40859 | 1221 |
lemma (in finite_measure) real_finite_measure_countably_subadditive: |
38656 | 1222 |
assumes "range f \<subseteq> sets M" and "summable (\<lambda>i. real (\<mu> (f i)))" |
1223 |
shows "real (\<mu> (\<Union>i. f i)) \<le> (\<Sum> i. real (\<mu> (f i)))" |
|
40859 | 1224 |
proof (rule real_measure_countably_subadditive[OF assms(1)]) |
38656 | 1225 |
have *: "\<And>i. f i \<in> sets M" using assms by auto |
1226 |
have "(\<lambda>i. real (\<mu> (f i))) sums (\<Sum>i. real (\<mu> (f i)))" |
|
1227 |
using assms(2) by (rule summable_sums) |
|
1228 |
from suminf_imp_psuminf[OF this] |
|
1229 |
have "(\<Sum>\<^isub>\<infinity>i. \<mu> (f i)) = Real (\<Sum>i. real (\<mu> (f i)))" |
|
1230 |
using * by (simp add: Real_real finite_measure) |
|
1231 |
thus "(\<Sum>\<^isub>\<infinity>i. \<mu> (f i)) \<noteq> \<omega>" by simp |
|
1232 |
qed |
|
1233 |
||
1234 |
lemma (in finite_measure) real_finite_measure_finite_singelton: |
|
1235 |
assumes "finite S" and *: "\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M" |
|
1236 |
shows "real (\<mu> S) = (\<Sum>x\<in>S. real (\<mu> {x}))" |
|
1237 |
proof (rule real_measure_setsum_singleton[OF `finite S`]) |
|
1238 |
fix x assume "x \<in> S" thus "{x} \<in> sets M" by (rule *) |
|
1239 |
with finite_measure show "\<mu> {x} \<noteq> \<omega>" . |
|
1240 |
qed |
|
1241 |
||
1242 |
lemma (in finite_measure) real_finite_continuity_from_below: |
|
1243 |
assumes "range A \<subseteq> sets M" "\<And>i. A i \<subseteq> A (Suc i)" |
|
1244 |
shows "(\<lambda>i. real (\<mu> (A i))) ----> real (\<mu> (\<Union>i. A i))" |
|
1245 |
using real_continuity_from_below[OF assms(1), OF assms(2) finite_measure] assms by auto |
|
1246 |
||
1247 |
lemma (in finite_measure) real_finite_continuity_from_above: |
|
1248 |
assumes A: "range A \<subseteq> sets M" |
|
1249 |
and mono_Suc: "\<And>n. A (Suc n) \<subseteq> A n" |
|
1250 |
shows "(\<lambda>n. real (\<mu> (A n))) ----> real (\<mu> (\<Inter>i. A i))" |
|
1251 |
using real_continuity_from_above[OF A, OF mono_Suc finite_measure] A |
|
1252 |
by auto |
|
1253 |
||
1254 |
lemma (in finite_measure) real_finite_measure_finite_Union': |
|
1255 |
assumes "finite S" "A`S \<subseteq> sets M" "disjoint_family_on A S" |
|
1256 |
shows "real (\<mu> (\<Union>i\<in>S. A i)) = (\<Sum>i\<in>S. real (\<mu> (A i)))" |
|
1257 |
using assms real_finite_measure_finite_Union[of S A] by auto |
|
1258 |
||
1259 |
lemma (in finite_measure) finite_measure_compl: |
|
1260 |
assumes s: "s \<in> sets M" |
|
1261 |
shows "\<mu> (space M - s) = \<mu> (space M) - \<mu> s" |
|
1262 |
using measure_compl[OF s, OF finite_measure, OF s] . |
|
1263 |
||
39092 | 1264 |
lemma (in finite_measure) finite_measure_inter_full_set: |
1265 |
assumes "S \<in> sets M" "T \<in> sets M" |
|
1266 |
assumes T: "\<mu> T = \<mu> (space M)" |
|
1267 |
shows "\<mu> (S \<inter> T) = \<mu> S" |
|
1268 |
using measure_inter_full_set[OF assms(1,2) finite_measure assms(3)] assms |
|
1269 |
by auto |
|
1270 |
||
38656 | 1271 |
section {* Measure preserving *} |
1272 |
||
1273 |
definition "measure_preserving A \<mu> B \<nu> = |
|
1274 |
{f \<in> measurable A B. (\<forall>y \<in> sets B. \<mu> (f -` y \<inter> space A) = \<nu> y)}" |
|
1275 |
||
1276 |
lemma (in finite_measure) measure_preserving_lift: |
|
40859 | 1277 |
fixes f :: "'a \<Rightarrow> 'a2" and A :: "'a2 algebra" |
38656 | 1278 |
assumes "algebra A" |
40859 | 1279 |
assumes "finite_measure (sigma A) \<nu>" (is "finite_measure ?sA _") |
38656 | 1280 |
assumes fmp: "f \<in> measure_preserving M \<mu> A \<nu>" |
40859 | 1281 |
shows "f \<in> measure_preserving M \<mu> (sigma A) \<nu>" |
38656 | 1282 |
proof - |
1283 |
interpret sA: finite_measure ?sA \<nu> by fact |
|
1284 |
interpret A: algebra A by fact |
|
1285 |
show ?thesis using fmp |
|
1286 |
proof (clarsimp simp add: measure_preserving_def) |
|
1287 |
assume fm: "f \<in> measurable M A" |
|
1288 |
and meq: "\<forall>y\<in>sets A. \<mu> (f -` y \<inter> space M) = \<nu> y" |
|
1289 |
have f12: "f \<in> measurable M ?sA" |
|
1290 |
using measurable_subset[OF A.sets_into_space] fm by auto |
|
1291 |
hence ffn: "f \<in> space M \<rightarrow> space A" |
|
1292 |
by (simp add: measurable_def) |
|
1293 |
have "space M \<subseteq> f -` (space A)" |
|
1294 |
by auto (metis PiE ffn) |
|
1295 |
hence fveq [simp]: "(f -` (space A)) \<inter> space M = space M" |
|
1296 |
by blast |
|
1297 |
{ |
|
1298 |
fix y |
|
1299 |
assume y: "y \<in> sets ?sA" |
|
1300 |
have "sets ?sA = sigma_sets (space A) (sets A)" (is "_ = ?A") by (auto simp: sigma_def) |
|
1301 |
also have "\<dots> \<subseteq> {s . \<mu> ((f -` s) \<inter> space M) = \<nu> s}" |
|
1302 |
proof (rule A.sigma_property_disjoint, auto) |
|
1303 |
fix x assume "x \<in> sets A" then show "\<mu> (f -` x \<inter> space M) = \<nu> x" by (simp add: meq) |
|
1304 |
next |
|
1305 |
fix s |
|
1306 |
assume eq: "\<mu> (f -` s \<inter> space M) = \<nu> s" and s: "s \<in> ?A" |
|
1307 |
then have s': "s \<in> sets ?sA" by (simp add: sigma_def) |
|
1308 |
show "\<mu> (f -` (space A - s) \<inter> space M) = \<nu> (space A - s)" |
|
1309 |
using sA.finite_measure_compl[OF s'] |
|
1310 |
using measurable_sets[OF f12 s'] meq[THEN bspec, OF A.top] |
|
1311 |
by (simp add: vimage_Diff Diff_Int_distrib2 finite_measure_compl eq) |
|
1312 |
next |
|
1313 |
fix S |
|
1314 |
assume S0: "S 0 = {}" |
|
1315 |
and SSuc: "\<And>n. S n \<subseteq> S (Suc n)" |
|
1316 |
and rS1: "range S \<subseteq> {s. \<mu> (f -` s \<inter> space M) = \<nu> s}" |
|
1317 |
and "range S \<subseteq> ?A" |
|
1318 |
hence rS2: "range S \<subseteq> sets ?sA" by (simp add: sigma_def) |
|
1319 |
have eq1: "\<And>i. \<mu> (f -` S i \<inter> space M) = \<nu> (S i)" |
|
1320 |
using rS1 by blast |
|
1321 |
have *: "(\<lambda>n. \<nu> (S n)) = (\<lambda>n. \<mu> (f -` S n \<inter> space M))" |
|
1322 |
by (simp add: eq1) |
|
1323 |
have "(SUP n. ... n) = \<mu> (\<Union>i. f -` S i \<inter> space M)" |
|
1324 |
proof (rule measure_countable_increasing) |
|
1325 |
show "range (\<lambda>i. f -` S i \<inter> space M) \<subseteq> sets M" |
|
1326 |
using f12 rS2 by (auto simp add: measurable_def) |
|
1327 |
show "f -` S 0 \<inter> space M = {}" using S0 |
|
1328 |
by blast |
|
1329 |
show "\<And>n. f -` S n \<inter> space M \<subseteq> f -` S (Suc n) \<inter> space M" |
|
1330 |
using SSuc by auto |
|
1331 |
qed |
|
1332 |
also have "\<mu> (\<Union>i. f -` S i \<inter> space M) = \<mu> (f -` (\<Union>i. S i) \<inter> space M)" |
|
1333 |
by (simp add: vimage_UN) |
|
1334 |
finally have "(SUP n. \<nu> (S n)) = \<mu> (f -` (\<Union>i. S i) \<inter> space M)" unfolding * . |
|
1335 |
moreover |
|
1336 |
have "(SUP n. \<nu> (S n)) = \<nu> (\<Union>i. S i)" |
|
1337 |
by (rule sA.measure_countable_increasing[OF rS2, OF S0 SSuc]) |
|
1338 |
ultimately |
|
1339 |
show "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<nu> (\<Union>i. S i)" by simp |
|
1340 |
next |
|
1341 |
fix S :: "nat => 'a2 set" |
|
1342 |
assume dS: "disjoint_family S" |
|
1343 |
and rS1: "range S \<subseteq> {s. \<mu> (f -` s \<inter> space M) = \<nu> s}" |
|
1344 |
and "range S \<subseteq> ?A" |
|
1345 |
hence rS2: "range S \<subseteq> sets ?sA" by (simp add: sigma_def) |
|
1346 |
have "\<And>i. \<mu> (f -` S i \<inter> space M) = \<nu> (S i)" |
|
1347 |
using rS1 by blast |
|
1348 |
hence *: "(\<lambda>i. \<nu> (S i)) = (\<lambda>n. \<mu> (f -` S n \<inter> space M))" |
|
1349 |
by simp |
|
1350 |
have "psuminf ... = \<mu> (\<Union>i. f -` S i \<inter> space M)" |
|
1351 |
proof (rule measure_countably_additive) |
|
1352 |
show "range (\<lambda>i. f -` S i \<inter> space M) \<subseteq> sets M" |
|
1353 |
using f12 rS2 by (auto simp add: measurable_def) |
|
1354 |
show "disjoint_family (\<lambda>i. f -` S i \<inter> space M)" using dS |
|
1355 |
by (auto simp add: disjoint_family_on_def) |
|
1356 |
qed |
|
1357 |
hence "(\<Sum>\<^isub>\<infinity> i. \<nu> (S i)) = \<mu> (\<Union>i. f -` S i \<inter> space M)" unfolding * . |
|
1358 |
with sA.measure_countably_additive [OF rS2 dS] |
|
1359 |
have "\<mu> (\<Union>i. f -` S i \<inter> space M) = \<nu> (\<Union>i. S i)" |
|
1360 |
by simp |
|
1361 |
moreover have "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<mu> (\<Union>i. f -` S i \<inter> space M)" |
|
1362 |
by (simp add: vimage_UN) |
|
1363 |
ultimately show "\<mu> (f -` (\<Union>i. S i) \<inter> space M) = \<nu> (\<Union>i. S i)" |
|
1364 |
by metis |
|
1365 |
qed |
|
1366 |
finally have "sets ?sA \<subseteq> {s . \<mu> ((f -` s) \<inter> space M) = \<nu> s}" . |
|
1367 |
hence "\<mu> (f -` y \<inter> space M) = \<nu> y" using y by force |
|
1368 |
} |
|
1369 |
thus "f \<in> measurable M ?sA \<and> (\<forall>y\<in>sets ?sA. \<mu> (f -` y \<inter> space M) = \<nu> y)" |
|
1370 |
by (blast intro: f12) |
|
1371 |
qed |
|
1372 |
qed |
|
1373 |
||
1374 |
section "Finite spaces" |
|
1375 |
||
40859 | 1376 |
locale finite_measure_space = measure_space + finite_sigma_algebra + |
1377 |
assumes finite_single_measure[simp]: "\<And>x. x \<in> space M \<Longrightarrow> \<mu> {x} \<noteq> \<omega>" |
|
39092 | 1378 |
|
38656 | 1379 |
lemma (in finite_measure_space) sum_over_space: "(\<Sum>x\<in>space M. \<mu> {x}) = \<mu> (space M)" |
36624 | 1380 |
using measure_finitely_additive''[of "space M" "\<lambda>i. {i}"] |
1381 |
by (simp add: sets_eq_Pow disjoint_family_on_def finite_space) |
|
1382 |
||
39092 | 1383 |
lemma finite_measure_spaceI: |
1384 |
assumes "finite (space M)" "sets M = Pow(space M)" and space: "\<mu> (space M) \<noteq> \<omega>" |
|
1385 |
and add: "\<And>A B. A\<subseteq>space M \<Longrightarrow> B\<subseteq>space M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow> \<mu> (A \<union> B) = \<mu> A + \<mu> B" |
|
1386 |
and "\<mu> {} = 0" |
|
1387 |
shows "finite_measure_space M \<mu>" |
|
1388 |
unfolding finite_measure_space_def finite_measure_space_axioms_def |
|
40859 | 1389 |
proof (intro allI impI conjI) |
39092 | 1390 |
show "measure_space M \<mu>" |
1391 |
proof (rule sigma_algebra.finite_additivity_sufficient) |
|
40859 | 1392 |
have *: "\<lparr>space = space M, sets = sets M\<rparr> = M" by auto |
39092 | 1393 |
show "sigma_algebra M" |
40859 | 1394 |
using sigma_algebra_Pow[of "space M" "more M"] assms(2)[symmetric] by (simp add: *) |
39092 | 1395 |
show "finite (space M)" by fact |
1396 |
show "positive \<mu>" unfolding positive_def by fact |
|
1397 |
show "additive M \<mu>" unfolding additive_def using assms by simp |
|
1398 |
qed |
|
40859 | 1399 |
then interpret measure_space M \<mu> . |
1400 |
show "finite_sigma_algebra M" |
|
1401 |
proof |
|
1402 |
show "finite (space M)" by fact |
|
1403 |
show "sets M = Pow (space M)" using assms by auto |
|
1404 |
qed |
|
39092 | 1405 |
{ fix x assume *: "x \<in> space M" |
1406 |
with add[of "{x}" "space M - {x}"] space |
|
1407 |
show "\<mu> {x} \<noteq> \<omega>" by (auto simp: insert_absorb[OF *] Diff_subset) } |
|
1408 |
qed |
|
1409 |
||
40871 | 1410 |
sublocale finite_measure_space \<subseteq> finite_measure |
38656 | 1411 |
proof |
1412 |
show "\<mu> (space M) \<noteq> \<omega>" |
|
1413 |
unfolding sum_over_space[symmetric] setsum_\<omega> |
|
1414 |
using finite_space finite_single_measure by auto |
|
1415 |
qed |
|
1416 |
||
39092 | 1417 |
lemma finite_measure_space_iff: |
1418 |
"finite_measure_space M \<mu> \<longleftrightarrow> |
|
1419 |
finite (space M) \<and> sets M = Pow(space M) \<and> \<mu> (space M) \<noteq> \<omega> \<and> \<mu> {} = 0 \<and> |
|
1420 |
(\<forall>A\<subseteq>space M. \<forall>B\<subseteq>space M. A \<inter> B = {} \<longrightarrow> \<mu> (A \<union> B) = \<mu> A + \<mu> B)" |
|
1421 |
(is "_ = ?rhs") |
|
1422 |
proof (intro iffI) |
|
1423 |
assume "finite_measure_space M \<mu>" |
|
1424 |
then interpret finite_measure_space M \<mu> . |
|
1425 |
show ?rhs |
|
1426 |
using finite_space sets_eq_Pow measure_additive empty_measure finite_measure |
|
1427 |
by auto |
|
1428 |
next |
|
1429 |
assume ?rhs then show "finite_measure_space M \<mu>" |
|
1430 |
by (auto intro!: finite_measure_spaceI) |
|
1431 |
qed |
|
1432 |
||
38656 | 1433 |
lemma psuminf_cmult_indicator: |
1434 |
assumes "disjoint_family A" "x \<in> A i" |
|
1435 |
shows "(\<Sum>\<^isub>\<infinity> n. f n * indicator (A n) x) = f i" |
|
1436 |
proof - |
|
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1437 |
have **: "\<And>n. f n * indicator (A n) x = (if n = i then f n else 0 :: pextreal)" |
38656 | 1438 |
using `x \<in> A i` assms unfolding disjoint_family_on_def indicator_def by auto |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1439 |
then have "\<And>n. (\<Sum>j<n. f j * indicator (A j) x) = (if i < n then f i else 0 :: pextreal)" |
38656 | 1440 |
by (auto simp: setsum_cases) |
41023
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1441 |
moreover have "(SUP n. if i < n then f i else 0) = (f i :: pextreal)" |
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1442 |
proof (rule pextreal_SUPI) |
9118eb4eb8dc
it is known as the extended reals, not the infinite reals
hoelzl
parents:
40871
diff
changeset
|
1443 |
fix y :: pextreal assume "\<And>n. n \<in> UNIV \<Longrightarrow> (if i < n then f i else 0) \<le> y" |
38656 | 1444 |
from this[of "Suc i"] show "f i \<le> y" by auto |
1445 |
qed simp |
|
1446 |
ultimately show ?thesis using `x \<in> A i` unfolding psuminf_def by auto |
|
1447 |
qed |
|
1448 |
||
1449 |
lemma psuminf_indicator: |
|
1450 |
assumes "disjoint_family A" |
|
1451 |
shows "(\<Sum>\<^isub>\<infinity> n. indicator (A n) x) = indicator (\<Union>i. A i) x" |
|
1452 |
proof cases |
|
1453 |
assume *: "x \<in> (\<Union>i. A i)" |
|
1454 |
then obtain i where "x \<in> A i" by auto |
|
1455 |
from psuminf_cmult_indicator[OF assms, OF this, of "\<lambda>i. 1"] |
|
1456 |
show ?thesis using * by simp |
|
1457 |
qed simp |
|
1458 |
||
35582 | 1459 |
end |