src/HOL/Probability/Measure_Space.thy
changeset 50087 635d73673b5e
parent 50002 ce0d316b5b44
child 50104 de19856feb54
     1.1 --- a/src/HOL/Probability/Measure_Space.thy	Thu Nov 15 14:04:23 2012 +0100
     1.2 +++ b/src/HOL/Probability/Measure_Space.thy	Thu Nov 15 10:49:58 2012 +0100
     1.3 @@ -169,6 +169,27 @@
     1.4    finally show "f x \<le> f y" by simp
     1.5  qed
     1.6  
     1.7 +lemma (in ring_of_sets) subadditive:
     1.8 +  assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> M" and S: "finite S"
     1.9 +  shows "f (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. f (A i))"
    1.10 +using S
    1.11 +proof (induct S)
    1.12 +  case empty thus ?case using f by (auto simp: positive_def)
    1.13 +next
    1.14 +  case (insert x F)
    1.15 +  hence in_M: "A x \<in> M" "(\<Union> i\<in>F. A i) \<in> M" "(\<Union> i\<in>F. A i) - A x \<in> M" using A by force+
    1.16 +  have subs: "(\<Union> i\<in>F. A i) - A x \<subseteq> (\<Union> i\<in>F. A i)" by auto
    1.17 +  have "(\<Union> i\<in>(insert x F). A i) = A x \<union> ((\<Union> i\<in>F. A i) - A x)" by auto
    1.18 +  hence "f (\<Union> i\<in>(insert x F). A i) = f (A x \<union> ((\<Union> i\<in>F. A i) - A x))"
    1.19 +    by simp
    1.20 +  also have "\<dots> = f (A x) + f ((\<Union> i\<in>F. A i) - A x)"
    1.21 +    using f(2) by (rule additiveD) (insert in_M, auto)
    1.22 +  also have "\<dots> \<le> f (A x) + f (\<Union> i\<in>F. A i)"
    1.23 +    using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono)
    1.24 +  also have "\<dots> \<le> f (A x) + (\<Sum>i\<in>F. f (A i))" using insert by (auto intro: add_left_mono)
    1.25 +  finally show "f (\<Union> i\<in>(insert x F). A i) \<le> (\<Sum>i\<in>(insert x F). f (A i))" using insert by simp
    1.26 +qed
    1.27 +
    1.28  lemma (in ring_of_sets) countably_additive_additive:
    1.29    assumes posf: "positive M f" and ca: "countably_additive M f"
    1.30    shows "additive M f"