src/HOL/Probability/Caratheodory.thy
 changeset 39096 111756225292 parent 38656 d5d342611edb child 40859 de0b30e6c2d2
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Thu Sep 02 17:12:40 2010 +0200
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Thu Sep 02 17:28:00 2010 +0200
1.3 @@ -445,21 +445,6 @@
1.4      by intro_locales (auto simp add: sigma_algebra_def)
1.5  qed
1.6
1.7 -
1.8 -lemma (in algebra) inf_measure_nonempty:
1.9 -  assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
1.10 -  shows "f b \<in> measure_set M f a"
1.11 -proof -
1.12 -  have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
1.13 -    by (rule psuminf_finite) (simp add: f[unfolded positive_def])
1.14 -  also have "... = f b"
1.15 -    by simp
1.16 -  finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
1.17 -  thus ?thesis using a b
1.18 -    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
1.19 -             simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
1.20 -qed
1.21 -
1.22  lemma (in algebra) additive_increasing:
1.23    assumes posf: "positive f" and addf: "additive M f"
1.24    shows "increasing M f"
1.25 @@ -494,6 +479,20 @@
1.26      by (auto simp add: Un binaryset_psuminf positive_def)
1.27  qed
1.28
1.29 +lemma inf_measure_nonempty:
1.30 +  assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b" "{} \<in> sets M"
1.31 +  shows "f b \<in> measure_set M f a"
1.32 +proof -
1.33 +  have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
1.34 +    by (rule psuminf_finite) (simp add: f[unfolded positive_def])
1.35 +  also have "... = f b"
1.36 +    by simp
1.37 +  finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
1.38 +  thus ?thesis using assms
1.39 +    by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
1.40 +             simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
1.41 +qed
1.42 +
1.43  lemma (in algebra) inf_measure_agrees:
1.44    assumes posf: "positive f" and ca: "countably_additive M f"
1.45        and s: "s \<in> sets M"
1.46 @@ -535,11 +534,11 @@
1.47  qed
1.48
1.49  lemma (in algebra) inf_measure_empty:
1.50 -  assumes posf: "positive f"
1.51 +  assumes posf: "positive f"  "{} \<in> sets M"
1.52    shows "Inf (measure_set M f {}) = 0"
1.53  proof (rule antisym)
1.54    show "Inf (measure_set M f {}) \<le> 0"
1.55 -    by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
1.56 +    by (metis complete_lattice_class.Inf_lower `{} \<in> sets M` inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
1.57  qed simp
1.58
1.59  lemma (in algebra) inf_measure_positive:
1.60 @@ -597,7 +596,7 @@
1.61  next
1.62    case True
1.63    have "measure_set M f s \<noteq> {}"
1.64 -    by (metis emptyE ss inf_measure_nonempty [of f, OF posf top])
1.65 +    by (metis emptyE ss inf_measure_nonempty [of f, OF posf top _ empty_sets])
1.66    then obtain l where "l \<in> measure_set M f s" by auto
1.67    moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
1.68    ultimately show ?thesis
```