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)"