summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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"