src/HOL/Analysis/Measure_Space.thy
changeset 67989 706f86afff43
parent 67982 7643b005b29a
child 68046 6aba668aea78
     1.1 --- a/src/HOL/Analysis/Measure_Space.thy	Mon Apr 16 05:34:25 2018 +0000
     1.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Mon Apr 16 15:00:46 2018 +0100
     1.3 @@ -1749,6 +1749,8 @@
     1.4      using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset)
     1.5  qed
     1.6  
     1.7 +subsection\<open>Measurable sets formed by unions and intersections\<close>
     1.8 +
     1.9  lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
    1.10    using fmeasurableI2[of A M "A - B"] by auto
    1.11  
    1.12 @@ -1882,15 +1884,20 @@
    1.13    "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> sets M) \<Longrightarrow> measure M (\<Union>F) \<le> (\<Sum>S\<in>F. measure M S)"
    1.14    using measure_UNION_le[of F "\<lambda>x. x" M] by simp
    1.15  
    1.16 +text\<open>Version for indexed union over a countable set\<close>
    1.17  lemma
    1.18    assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> fmeasurable M"
    1.19 -    and bound: "\<And>I'. I' \<subseteq> I \<Longrightarrow> finite I' \<Longrightarrow> measure M (\<Union>i\<in>I'. A i) \<le> B" and "0 \<le> B"
    1.20 +    and bound: "\<And>I'. I' \<subseteq> I \<Longrightarrow> finite I' \<Longrightarrow> measure M (\<Union>i\<in>I'. A i) \<le> B"
    1.21    shows fmeasurable_UN_bound: "(\<Union>i\<in>I. A i) \<in> fmeasurable M" (is ?fm)
    1.22      and measure_UN_bound: "measure M (\<Union>i\<in>I. A i) \<le> B" (is ?m)
    1.23  proof -
    1.24 +  have "B \<ge> 0"
    1.25 +    using bound by force
    1.26    have "?fm \<and> ?m"
    1.27    proof cases
    1.28 -    assume "I = {}" with \<open>0 \<le> B\<close> show ?thesis by simp
    1.29 +    assume "I = {}"
    1.30 +    with \<open>B \<ge> 0\<close> show ?thesis
    1.31 +      by simp
    1.32    next
    1.33      assume "I \<noteq> {}"
    1.34      have "(\<Union>i\<in>I. A i) = (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))"
    1.35 @@ -1918,6 +1925,58 @@
    1.36    then show ?fm ?m by auto
    1.37  qed
    1.38  
    1.39 +text\<open>Version for big union of a countable set\<close>
    1.40 +lemma
    1.41 +  assumes "countable \<D>"
    1.42 +    and meas: "\<And>D. D \<in> \<D> \<Longrightarrow> D \<in> fmeasurable M"
    1.43 +    and bound:  "\<And>\<E>. \<lbrakk>\<E> \<subseteq> \<D>; finite \<E>\<rbrakk> \<Longrightarrow> measure M (\<Union>\<E>) \<le> B"
    1.44 + shows fmeasurable_Union_bound: "\<Union>\<D> \<in> fmeasurable M"  (is ?fm)
    1.45 +    and measure_Union_bound: "measure M (\<Union>\<D>) \<le> B"     (is ?m)
    1.46 +proof -
    1.47 +  have "B \<ge> 0"
    1.48 +    using bound by force
    1.49 +  have "?fm \<and> ?m"
    1.50 +  proof (cases "\<D> = {}")
    1.51 +    case True
    1.52 +    with \<open>B \<ge> 0\<close> show ?thesis
    1.53 +      by auto
    1.54 +  next
    1.55 +    case False
    1.56 +    then obtain D :: "nat \<Rightarrow> 'a set" where D: "\<D> = range D"
    1.57 +      using \<open>countable \<D>\<close> uncountable_def by force
    1.58 +      have 1: "\<And>i. D i \<in> fmeasurable M"
    1.59 +        by (simp add: D meas)
    1.60 +      have 2: "\<And>I'. finite I' \<Longrightarrow> measure M (\<Union>x\<in>I'. D x) \<le> B"
    1.61 +        by (simp add: D bound image_subset_iff)
    1.62 +      show ?thesis
    1.63 +        unfolding D
    1.64 +        by (intro conjI fmeasurable_UN_bound [OF _ 1 2] measure_UN_bound [OF _ 1 2]) auto
    1.65 +    qed
    1.66 +    then show ?fm ?m by auto
    1.67 +qed
    1.68 +
    1.69 +text\<open>Version for indexed union over the type of naturals\<close>
    1.70 +lemma
    1.71 +  fixes S :: "nat \<Rightarrow> 'a set"
    1.72 +  assumes S: "\<And>i. S i \<in> fmeasurable M" and B: "\<And>n. measure M (\<Union>i\<le>n. S i) \<le> B"
    1.73 +  shows fmeasurable_countable_Union: "(\<Union>i. S i) \<in> fmeasurable M"
    1.74 +    and measure_countable_Union_le: "measure M (\<Union>i. S i) \<le> B"
    1.75 +proof -
    1.76 +  have mB: "measure M (\<Union>i\<in>I. S i) \<le> B" if "finite I" for I
    1.77 +  proof -
    1.78 +    have "(\<Union>i\<in>I. S i) \<subseteq> (\<Union>i\<le>Max I. S i)"
    1.79 +      using Max_ge that by force
    1.80 +    then have "measure M (\<Union>i\<in>I. S i) \<le> measure M (\<Union>i \<le> Max I. S i)"
    1.81 +      by (rule measure_mono_fmeasurable) (use S in \<open>blast+\<close>)
    1.82 +    then show ?thesis
    1.83 +      using B order_trans by blast
    1.84 +  qed
    1.85 +  show "(\<Union>i. S i) \<in> fmeasurable M"
    1.86 +    by (auto intro: fmeasurable_UN_bound [OF _ S mB])
    1.87 +  show "measure M (\<Union>n. S n) \<le> B"
    1.88 +    by (auto intro: measure_UN_bound [OF _ S mB])
    1.89 +qed
    1.90 +
    1.91  lemma measure_diff_le_measure_setdiff:
    1.92    assumes "S \<in> fmeasurable M" "T \<in> fmeasurable M"
    1.93    shows "measure M S - measure M T \<le> measure M (S - T)"