diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy Mon Apr 16 05:34:25 2018 +0000
+++ b/src/HOL/Analysis/Measure_Space.thy Mon Apr 16 15:00:46 2018 +0100
@@ -1749,6 +1749,8 @@
using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset)
qed
+subsection\Measurable sets formed by unions and intersections\
+
lemma fmeasurable_Diff: "A \ fmeasurable M \ B \ sets M \ A - B \ fmeasurable M"
using fmeasurableI2[of A M "A - B"] by auto
@@ -1882,15 +1884,20 @@
"finite F \ (\S. S \ F \ S \ sets M) \ measure M (\F) \ (\S\F. measure M S)"
using measure_UNION_le[of F "\x. x" M] by simp
+text\Version for indexed union over a countable set\
lemma
assumes "countable I" and I: "\i. i \ I \ A i \ fmeasurable M"
- and bound: "\I'. I' \ I \ finite I' \ measure M (\i\I'. A i) \ B" and "0 \ B"
+ and bound: "\I'. I' \ I \ finite I' \ measure M (\i\I'. A i) \ B"
shows fmeasurable_UN_bound: "(\i\I. A i) \ fmeasurable M" (is ?fm)
and measure_UN_bound: "measure M (\i\I. A i) \ B" (is ?m)
proof -
+ have "B \ 0"
+ using bound by force
have "?fm \ ?m"
proof cases
- assume "I = {}" with \0 \ B\ show ?thesis by simp
+ assume "I = {}"
+ with \B \ 0\ show ?thesis
+ by simp
next
assume "I \ {}"
have "(\i\I. A i) = (\i. (\n\i. A (from_nat_into I n)))"
@@ -1918,6 +1925,58 @@
then show ?fm ?m by auto
qed
+text\Version for big union of a countable set\
+lemma
+ assumes "countable \"
+ and meas: "\D. D \ \ \ D \ fmeasurable M"
+ and bound: "\\. \\ \ \; finite \\ \ measure M (\\) \ B"
+ shows fmeasurable_Union_bound: "\\ \ fmeasurable M" (is ?fm)
+ and measure_Union_bound: "measure M (\\) \ B" (is ?m)
+proof -
+ have "B \ 0"
+ using bound by force
+ have "?fm \ ?m"
+ proof (cases "\ = {}")
+ case True
+ with \B \ 0\ show ?thesis
+ by auto
+ next
+ case False
+ then obtain D :: "nat \ 'a set" where D: "\ = range D"
+ using \countable \\ uncountable_def by force
+ have 1: "\i. D i \ fmeasurable M"
+ by (simp add: D meas)
+ have 2: "\I'. finite I' \ measure M (\x\I'. D x) \ B"
+ by (simp add: D bound image_subset_iff)
+ show ?thesis
+ unfolding D
+ by (intro conjI fmeasurable_UN_bound [OF _ 1 2] measure_UN_bound [OF _ 1 2]) auto
+ qed
+ then show ?fm ?m by auto
+qed
+
+text\Version for indexed union over the type of naturals\
+lemma
+ fixes S :: "nat \ 'a set"
+ assumes S: "\i. S i \ fmeasurable M" and B: "\n. measure M (\i\n. S i) \ B"
+ shows fmeasurable_countable_Union: "(\i. S i) \ fmeasurable M"
+ and measure_countable_Union_le: "measure M (\i. S i) \ B"
+proof -
+ have mB: "measure M (\i\I. S i) \ B" if "finite I" for I
+ proof -
+ have "(\i\I. S i) \ (\i\Max I. S i)"
+ using Max_ge that by force
+ then have "measure M (\i\I. S i) \ measure M (\i \ Max I. S i)"
+ by (rule measure_mono_fmeasurable) (use S in \blast+\)
+ then show ?thesis
+ using B order_trans by blast
+ qed
+ show "(\i. S i) \ fmeasurable M"
+ by (auto intro: fmeasurable_UN_bound [OF _ S mB])
+ show "measure M (\n. S n) \ B"
+ by (auto intro: measure_UN_bound [OF _ S mB])
+qed
+
lemma measure_diff_le_measure_setdiff:
assumes "S \ fmeasurable M" "T \ fmeasurable M"
shows "measure M S - measure M T \ measure M (S - T)"