diff -r ecffea78d381 -r 635d73673b5e src/HOL/Probability/Measure_Space.thy --- a/src/HOL/Probability/Measure_Space.thy Thu Nov 15 14:04:23 2012 +0100 +++ b/src/HOL/Probability/Measure_Space.thy Thu Nov 15 10:49:58 2012 +0100 @@ -169,6 +169,27 @@ finally show "f x \ f y" by simp qed +lemma (in ring_of_sets) subadditive: + assumes f: "positive M f" "additive M f" and A: "range A \ M" and S: "finite S" + shows "f (\i\S. A i) \ (\i\S. f (A i))" +using S +proof (induct S) + case empty thus ?case using f by (auto simp: positive_def) +next + case (insert x F) + hence in_M: "A x \ M" "(\ i\F. A i) \ M" "(\ i\F. A i) - A x \ M" using A by force+ + have subs: "(\ i\F. A i) - A x \ (\ i\F. A i)" by auto + have "(\ i\(insert x F). A i) = A x \ ((\ i\F. A i) - A x)" by auto + hence "f (\ i\(insert x F). A i) = f (A x \ ((\ i\F. A i) - A x))" + by simp + also have "\ = f (A x) + f ((\ i\F. A i) - A x)" + using f(2) by (rule additiveD) (insert in_M, auto) + also have "\ \ f (A x) + f (\ i\F. A i)" + using additive_increasing[OF f] in_M subs by (auto simp: increasing_def intro: add_left_mono) + also have "\ \ f (A x) + (\i\F. f (A i))" using insert by (auto intro: add_left_mono) + finally show "f (\ i\(insert x F). A i) \ (\i\(insert x F). f (A i))" using insert by simp +qed + lemma (in ring_of_sets) countably_additive_additive: assumes posf: "positive M f" and ca: "countably_additive M f" shows "additive M f"