--- a/src/HOL/Probability/Caratheodory.thy Thu Sep 02 17:12:40 2010 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Thu Sep 02 17:28:00 2010 +0200
@@ -445,21 +445,6 @@
by intro_locales (auto simp add: sigma_algebra_def)
qed
-
-lemma (in algebra) inf_measure_nonempty:
- assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
- shows "f b \<in> measure_set M f a"
-proof -
- have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
- by (rule psuminf_finite) (simp add: f[unfolded positive_def])
- also have "... = f b"
- by simp
- finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
- thus ?thesis using a b
- by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
- simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
-qed
-
lemma (in algebra) additive_increasing:
assumes posf: "positive f" and addf: "additive M f"
shows "increasing M f"
@@ -494,6 +479,20 @@
by (auto simp add: Un binaryset_psuminf positive_def)
qed
+lemma inf_measure_nonempty:
+ assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b" "{} \<in> sets M"
+ shows "f b \<in> measure_set M f a"
+proof -
+ have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
+ by (rule psuminf_finite) (simp add: f[unfolded positive_def])
+ also have "... = f b"
+ by simp
+ finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
+ thus ?thesis using assms
+ by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
+ simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
+qed
+
lemma (in algebra) inf_measure_agrees:
assumes posf: "positive f" and ca: "countably_additive M f"
and s: "s \<in> sets M"
@@ -535,11 +534,11 @@
qed
lemma (in algebra) inf_measure_empty:
- assumes posf: "positive f"
+ assumes posf: "positive f" "{} \<in> sets M"
shows "Inf (measure_set M f {}) = 0"
proof (rule antisym)
show "Inf (measure_set M f {}) \<le> 0"
- by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
+ by (metis complete_lattice_class.Inf_lower `{} \<in> sets M` inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
qed simp
lemma (in algebra) inf_measure_positive:
@@ -597,7 +596,7 @@
next
case True
have "measure_set M f s \<noteq> {}"
- by (metis emptyE ss inf_measure_nonempty [of f, OF posf top])
+ by (metis emptyE ss inf_measure_nonempty [of f, OF posf top _ empty_sets])
then obtain l where "l \<in> measure_set M f s" by auto
moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
ultimately show ?thesis