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