HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
authorhoelzl
Thu Sep 29 18:52:34 2016 +0200 (2016-09-29)
changeset 63959f77dca1abf1b
parent 63958 02de4a58e210
child 63960 3daf02070be5
HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)
src/HOL/Analysis/Complete_Measure.thy
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/Analysis/Complete_Measure.thy	Thu Sep 29 13:54:57 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complete_Measure.thy	Thu Sep 29 18:52:34 2016 +0200
     1.3 @@ -794,6 +794,27 @@
     1.4  lemma (in complete_measure) complete2: "A \<subseteq> B \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> A \<in> null_sets M"
     1.5    using complete[of A B] null_sets_subset[of A B M] by simp
     1.6  
     1.7 +lemma (in complete_measure) AE_iff_null_sets: "(AE x in M. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets M"
     1.8 +  unfolding eventually_ae_filter by (auto intro: complete2)
     1.9 +
    1.10 +lemma (in complete_measure) null_sets_iff_AE: "A \<in> null_sets M \<longleftrightarrow> ((AE x in M. x \<notin> A) \<and> A \<subseteq> space M)"
    1.11 +  unfolding AE_iff_null_sets by (auto cong: rev_conj_cong dest: sets.sets_into_space simp: subset_eq)
    1.12 +
    1.13 +lemma (in complete_measure) in_sets_AE:
    1.14 +  assumes ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B" and A: "A \<in> sets M" and B: "B \<subseteq> space M"
    1.15 +  shows "B \<in> sets M"
    1.16 +proof -
    1.17 +  have "(AE x in M. x \<notin> B - A \<and> x \<notin> A - B)"
    1.18 +    using ae by eventually_elim auto
    1.19 +  then have "B - A \<in> null_sets M" "A - B \<in> null_sets M"
    1.20 +    using A B unfolding null_sets_iff_AE by (auto dest: sets.sets_into_space)
    1.21 +  then have "A \<union> (B - A) - (A - B) \<in> sets M"
    1.22 +    using A by blast
    1.23 +  also have "A \<union> (B - A) - (A - B) = B"
    1.24 +    by auto
    1.25 +  finally show "B \<in> sets M" .
    1.26 +qed
    1.27 +
    1.28  lemma (in complete_measure) vimage_null_part_null_sets:
    1.29    assumes f: "f \<in> M \<rightarrow>\<^sub>M N" and eq: "null_sets N \<subseteq> null_sets (distr M N f)"
    1.30      and A: "A \<in> completion N"
    1.31 @@ -955,6 +976,16 @@
    1.32      by simp
    1.33  qed (auto intro!: bexI[of _ S])
    1.34  
    1.35 +lemma (in complete_measure) null_sets_outer:
    1.36 +  "S \<in> null_sets M \<longleftrightarrow> (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T < e)"
    1.37 +proof -
    1.38 +  have "S \<in> null_sets M \<longleftrightarrow> (S \<in> fmeasurable M \<and> 0 = measure M S)"
    1.39 +    by (auto simp: null_sets_def emeasure_eq_measure2 intro: fmeasurableI) (simp add: measure_def)
    1.40 +  also have "\<dots> = (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T < e)"
    1.41 +    unfolding fmeasurable_measure_inner_outer by auto
    1.42 +  finally show ?thesis .
    1.43 +qed
    1.44 +
    1.45  lemma (in cld_measure) notin_sets_outer_measure_of_cover:
    1.46    assumes E: "E \<subseteq> space M" "E \<notin> sets M"
    1.47    shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and>
     2.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 29 13:54:57 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 29 18:52:34 2016 +0200
     2.3 @@ -959,6 +959,27 @@
     2.4  lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
     2.5    by (auto simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
     2.6  
     2.7 +lemma
     2.8 +  assumes \<D>: "\<D> division_of S"
     2.9 +  shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
    2.10 +    and content_divsion: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
    2.11 +proof -
    2.12 +  { fix d1 d2 assume *: "d1 \<in> \<D>" "d2 \<in> \<D>" "d1 \<noteq> d2"
    2.13 +    then obtain a b c d where "d1 = cbox a b" "d2 = cbox c d"
    2.14 +      using division_ofD(4)[OF \<D>] by blast
    2.15 +    with division_ofD(5)[OF \<D> *]
    2.16 +    have "d1 \<in> sets lborel" "d2 \<in> sets lborel" "d1 \<inter> d2 \<subseteq> (cbox a b - box a b) \<union> (cbox c d - box c d)"
    2.17 +      by auto
    2.18 +    moreover have "(cbox a b - box a b) \<union> (cbox c d - box c d) \<in> null_sets lborel"
    2.19 +      by (intro null_sets.Un null_sets_cbox_Diff_box)
    2.20 +    ultimately have "d1 \<inter> d2 \<in> null_sets lborel"
    2.21 +      by (blast intro: null_sets_subset) }
    2.22 +  then show ?l ?m
    2.23 +    unfolding division_ofD(6)[OF \<D>, symmetric]
    2.24 +    using division_ofD(1,4)[OF \<D>]
    2.25 +    by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
    2.26 +qed
    2.27 +
    2.28  text \<open>This should be an abbreviation for negligible.\<close>
    2.29  lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
    2.30  proof
    2.31 @@ -982,6 +1003,127 @@
    2.32    qed auto
    2.33  qed
    2.34  
    2.35 +lemma starlike_negligible:
    2.36 +  assumes "closed S"
    2.37 +      and eq1: "\<And>c x. \<lbrakk>(a + c *\<^sub>R x) \<in> S; 0 \<le> c; a + x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
    2.38 +    shows "negligible S"
    2.39 +proof -
    2.40 +  have "negligible (op + (-a) ` S)"
    2.41 +  proof (subst negligible_on_intervals, intro allI)
    2.42 +    fix u v
    2.43 +    show "negligible (op + (- a) ` S \<inter> cbox u v)"
    2.44 +      unfolding negligible_iff_null_sets
    2.45 +      apply (rule starlike_negligible_compact)
    2.46 +       apply (simp add: assms closed_translation closed_Int_compact, clarify)
    2.47 +      by (metis eq1 minus_add_cancel)
    2.48 +  qed
    2.49 +  then show ?thesis
    2.50 +    by (rule negligible_translation_rev)
    2.51 +qed
    2.52 +
    2.53 +lemma starlike_negligible_strong:
    2.54 +  assumes "closed S"
    2.55 +      and star: "\<And>c x. \<lbrakk>0 \<le> c; c < 1; a+x \<in> S\<rbrakk> \<Longrightarrow> a + c *\<^sub>R x \<notin> S"
    2.56 +    shows "negligible S"
    2.57 +proof -
    2.58 +  show ?thesis
    2.59 +  proof (rule starlike_negligible [OF \<open>closed S\<close>, of a])
    2.60 +    fix c x
    2.61 +    assume cx: "a + c *\<^sub>R x \<in> S" "0 \<le> c" "a + x \<in> S"
    2.62 +    with star have "~ (c < 1)" by auto
    2.63 +    moreover have "~ (c > 1)"
    2.64 +      using star [of "1/c" "c *\<^sub>R x"] cx by force
    2.65 +    ultimately show "c = 1" by arith
    2.66 +  qed
    2.67 +qed
    2.68 +
    2.69 +subsection\<open>Applications\<close>
    2.70 +
    2.71 +lemma negligible_hyperplane:
    2.72 +  assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
    2.73 +proof -
    2.74 +  obtain x where x: "a \<bullet> x \<noteq> b"
    2.75 +    using assms
    2.76 +    apply auto
    2.77 +     apply (metis inner_eq_zero_iff inner_zero_right)
    2.78 +    using inner_zero_right by fastforce
    2.79 +  show ?thesis
    2.80 +    apply (rule starlike_negligible [OF closed_hyperplane, of x])
    2.81 +    using x apply (auto simp: algebra_simps)
    2.82 +    done
    2.83 +qed
    2.84 +
    2.85 +lemma negligible_lowdim:
    2.86 +  fixes S :: "'N :: euclidean_space set"
    2.87 +  assumes "dim S < DIM('N)"
    2.88 +    shows "negligible S"
    2.89 +proof -
    2.90 +  obtain a where "a \<noteq> 0" and a: "span S \<subseteq> {x. a \<bullet> x = 0}"
    2.91 +    using lowdim_subset_hyperplane [OF assms] by blast
    2.92 +  have "negligible (span S)"
    2.93 +    using \<open>a \<noteq> 0\<close> a negligible_hyperplane by (blast intro: negligible_subset)
    2.94 +  then show ?thesis
    2.95 +    using span_inc by (blast intro: negligible_subset)
    2.96 +qed
    2.97 +
    2.98 +proposition negligible_convex_frontier:
    2.99 +  fixes S :: "'N :: euclidean_space set"
   2.100 +  assumes "convex S"
   2.101 +    shows "negligible(frontier S)"
   2.102 +proof -
   2.103 +  have nf: "negligible(frontier S)" if "convex S" "0 \<in> S" for S :: "'N set"
   2.104 +  proof -
   2.105 +    obtain B where "B \<subseteq> S" and indB: "independent B"
   2.106 +               and spanB: "S \<subseteq> span B" and cardB: "card B = dim S"
   2.107 +      by (metis basis_exists)
   2.108 +    consider "dim S < DIM('N)" | "dim S = DIM('N)"
   2.109 +      using dim_subset_UNIV le_eq_less_or_eq by blast
   2.110 +    then show ?thesis
   2.111 +    proof cases
   2.112 +      case 1
   2.113 +      show ?thesis
   2.114 +        by (rule negligible_subset [of "closure S"])
   2.115 +           (simp_all add: Diff_subset frontier_def negligible_lowdim 1)
   2.116 +    next
   2.117 +      case 2
   2.118 +      obtain a where a: "a \<in> interior S"
   2.119 +        apply (rule interior_simplex_nonempty [OF indB])
   2.120 +          apply (simp add: indB independent_finite)
   2.121 +         apply (simp add: cardB 2)
   2.122 +        apply (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
   2.123 +        done
   2.124 +      show ?thesis
   2.125 +      proof (rule starlike_negligible_strong [where a=a])
   2.126 +        fix c::real and x
   2.127 +        have eq: "a + c *\<^sub>R x = (a + x) - (1 - c) *\<^sub>R ((a + x) - a)"
   2.128 +          by (simp add: algebra_simps)
   2.129 +        assume "0 \<le> c" "c < 1" "a + x \<in> frontier S"
   2.130 +        then show "a + c *\<^sub>R x \<notin> frontier S"
   2.131 +          apply (clarsimp simp: frontier_def)
   2.132 +          apply (subst eq)
   2.133 +          apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"], auto)
   2.134 +          done
   2.135 +      qed auto
   2.136 +    qed
   2.137 +  qed
   2.138 +  show ?thesis
   2.139 +  proof (cases "S = {}")
   2.140 +    case True then show ?thesis by auto
   2.141 +  next
   2.142 +    case False
   2.143 +    then obtain a where "a \<in> S" by auto
   2.144 +    show ?thesis
   2.145 +      using nf [of "(\<lambda>x. -a + x) ` S"]
   2.146 +      by (metis \<open>a \<in> S\<close> add.left_inverse assms convex_translation_eq frontier_translation
   2.147 +                image_eqI negligible_translation_rev)
   2.148 +  qed
   2.149 +qed
   2.150 +
   2.151 +corollary negligible_sphere: "negligible (sphere a e)"
   2.152 +  using frontier_cball negligible_convex_frontier convex_cball
   2.153 +  by (blast intro: negligible_subset)
   2.154 +
   2.155 +
   2.156  lemma non_negligible_UNIV [simp]: "\<not> negligible UNIV"
   2.157    unfolding negligible_iff_null_sets by (auto simp: null_sets_def emeasure_lborel_UNIV)
   2.158  
     3.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 29 13:54:57 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 29 18:52:34 2016 +0200
     3.3 @@ -8,7 +8,7 @@
     3.4  section \<open>Lebesgue measure\<close>
     3.5  
     3.6  theory Lebesgue_Measure
     3.7 -  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure
     3.8 +  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests
     3.9  begin
    3.10  
    3.11  subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
    3.12 @@ -695,6 +695,19 @@
    3.13    finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
    3.14  qed
    3.15  
    3.16 +lemma lebesgue_measurable_scaling[measurable]: "op *\<^sub>R x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
    3.17 +proof cases
    3.18 +  assume "x = 0"
    3.19 +  then have "op *\<^sub>R x = (\<lambda>x. 0::'a)"
    3.20 +    by (auto simp: fun_eq_iff)
    3.21 +  then show ?thesis by auto
    3.22 +next
    3.23 +  assume "x \<noteq> 0" then show ?thesis
    3.24 +    using lebesgue_affine_measurable[of "\<lambda>_. x" 0]
    3.25 +    unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation
    3.26 +    by (auto simp add: ac_simps)
    3.27 +qed
    3.28 +
    3.29  lemma
    3.30    fixes m :: real and \<delta> :: "'a::euclidean_space"
    3.31    defines "T r d x \<equiv> r *\<^sub>R x + d"
    3.32 @@ -884,4 +897,93 @@
    3.33    and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
    3.34    by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
    3.35  
    3.36 +lemma lmeasurable_compact: "compact S \<Longrightarrow> S \<in> lmeasurable"
    3.37 +  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
    3.38 +
    3.39 +lemma lmeasurable_open: "bounded S \<Longrightarrow> open S \<Longrightarrow> S \<in> lmeasurable"
    3.40 +  using emeasure_bounded_finite[of S] by (intro fmeasurableI) (auto simp: borel_open)
    3.41 +
    3.42 +lemma lmeasurable_ball: "ball a r \<in> lmeasurable"
    3.43 +  by (simp add: lmeasurable_open)
    3.44 +
    3.45 +lemma lmeasurable_interior: "bounded S \<Longrightarrow> interior S \<in> lmeasurable"
    3.46 +  by (simp add: bounded_interior lmeasurable_open)
    3.47 +
    3.48 +lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel"
    3.49 +proof -
    3.50 +  have "emeasure lborel (cbox a b - box a b) = 0"
    3.51 +    by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox)
    3.52 +  then have "cbox a b - box a b \<in> null_sets lborel"
    3.53 +    by (auto simp: null_sets_def)
    3.54 +  then show ?thesis
    3.55 +    by (auto dest!: AE_not_in)
    3.56 +qed
    3.57 +subsection\<open> A nice lemma for negligibility proofs.\<close>
    3.58 +
    3.59 +lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
    3.60 +  by (metis summable_suminf_not_top)
    3.61 +
    3.62 +proposition starlike_negligible_bounded_gmeasurable:
    3.63 +  fixes S :: "'a :: euclidean_space set"
    3.64 +  assumes S: "S \<in> sets lebesgue" and "bounded S"
    3.65 +      and eq1: "\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
    3.66 +    shows "S \<in> null_sets lebesgue"
    3.67 +proof -
    3.68 +  obtain M where "0 < M" "S \<subseteq> ball 0 M"
    3.69 +    using \<open>bounded S\<close> by (auto dest: bounded_subset_ballD)
    3.70 +
    3.71 +  let ?f = "\<lambda>n. root DIM('a) (Suc n)"
    3.72 +
    3.73 +  have vimage_eq_image: "op *\<^sub>R (?f n) -` S = op *\<^sub>R (1 / ?f n) ` S" for n
    3.74 +    apply safe
    3.75 +    subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
    3.76 +    subgoal by auto
    3.77 +    done
    3.78 +
    3.79 +  have eq: "(1 / ?f n) ^ DIM('a) = 1 / Suc n" for n
    3.80 +    by (simp add: field_simps)
    3.81 +
    3.82 +  { fix n x assume x: "root DIM('a) (1 + real n) *\<^sub>R x \<in> S"
    3.83 +    have "1 * norm x \<le> root DIM('a) (1 + real n) * norm x"
    3.84 +      by (rule mult_mono) auto
    3.85 +    also have "\<dots> < M"
    3.86 +      using x \<open>S \<subseteq> ball 0 M\<close> by auto
    3.87 +    finally have "norm x < M" by simp }
    3.88 +  note less_M = this
    3.89 +
    3.90 +  have "(\<Sum>n. ennreal (1 / Suc n)) = top"
    3.91 +    using not_summable_harmonic[where 'a=real] summable_Suc_iff[where f="\<lambda>n. 1 / (real n)"]
    3.92 +    by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
    3.93 +  then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
    3.94 +    unfolding ennreal_suminf_multc eq by simp
    3.95 +  also have "\<dots> = (\<Sum>n. emeasure lebesgue (op *\<^sub>R (?f n) -` S))"
    3.96 +    unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
    3.97 +  also have "\<dots> = emeasure lebesgue (\<Union>n. op *\<^sub>R (?f n) -` S)"
    3.98 +  proof (intro suminf_emeasure)
    3.99 +    show "disjoint_family (\<lambda>n. op *\<^sub>R (?f n) -` S)"
   3.100 +      unfolding disjoint_family_on_def
   3.101 +    proof safe
   3.102 +      fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
   3.103 +      with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
   3.104 +        by auto
   3.105 +    qed
   3.106 +    have "op *\<^sub>R (?f i) -` S \<in> sets lebesgue" for i
   3.107 +      using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
   3.108 +    then show "range (\<lambda>i. op *\<^sub>R (?f i) -` S) \<subseteq> sets lebesgue"
   3.109 +      by auto
   3.110 +  qed
   3.111 +  also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"
   3.112 +    using less_M by (intro emeasure_mono) auto
   3.113 +  also have "\<dots> < top"
   3.114 +    using lmeasurable_ball by (auto simp: fmeasurable_def)
   3.115 +  finally have "emeasure lebesgue S = 0"
   3.116 +    by (simp add: ennreal_top_mult split: if_split_asm)
   3.117 +  then show "S \<in> null_sets lebesgue"
   3.118 +    unfolding null_sets_def using \<open>S \<in> sets lebesgue\<close> by auto
   3.119 +qed
   3.120 +
   3.121 +corollary starlike_negligible_compact:
   3.122 +  "compact S \<Longrightarrow> (\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1) \<Longrightarrow> S \<in> null_sets lebesgue"
   3.123 +  using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed)
   3.124 +
   3.125  end
     4.1 --- a/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 13:54:57 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 18:52:34 2016 +0200
     4.3 @@ -1127,6 +1127,12 @@
     4.4      unfolding eventually_ae_filter by auto
     4.5  qed auto
     4.6  
     4.7 +lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
     4.8 +  by (auto simp add: pairwise_def)
     4.9 +
    4.10 +lemma AE_pairwise: "countable F \<Longrightarrow> pairwise (\<lambda>A B. AE x in M. R x A B) F \<longleftrightarrow> (AE x in M. pairwise (R x) F)"
    4.11 +  unfolding pairwise_alt by (simp add: AE_ball_countable)
    4.12 +
    4.13  lemma AE_discrete_difference:
    4.14    assumes X: "countable X"
    4.15    assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
    4.16 @@ -1453,6 +1459,12 @@
    4.17    by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top
    4.18             del: real_of_ereal_enn2ereal)
    4.19  
    4.20 +lemma measure_eq_AE:
    4.21 +  assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
    4.22 +  assumes A: "A \<in> sets M" and B: "B \<in> sets M"
    4.23 +  shows "measure M A = measure M B"
    4.24 +  using assms emeasure_eq_AE[OF assms] by (simp add: measure_def)
    4.25 +
    4.26  lemma measure_Union:
    4.27    "emeasure M A \<noteq> \<infinity> \<Longrightarrow> emeasure M B \<noteq> \<infinity> \<Longrightarrow> A \<in> sets M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A \<inter> B = {} \<Longrightarrow>
    4.28      measure M (A \<union> B) = measure M A + measure M B"
    4.29 @@ -1554,6 +1566,12 @@
    4.30      done
    4.31  qed
    4.32  
    4.33 +lemma measure_Un_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A \<union> B) = measure M A"
    4.34 +  by (simp add: measure_def emeasure_Un_null_set)
    4.35 +
    4.36 +lemma measure_Diff_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A - B) = measure M A"
    4.37 +  by (simp add: measure_def emeasure_Diff_null_set)
    4.38 +
    4.39  lemma measure_eq_setsum_singleton:
    4.40    "finite S \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> {x} \<in> sets M) \<Longrightarrow> (\<And>x. x \<in> S \<Longrightarrow> emeasure M {x} \<noteq> \<infinity>) \<Longrightarrow>
    4.41      measure M S = (\<Sum>x\<in>S. measure M {x})"
    4.42 @@ -1595,6 +1613,9 @@
    4.43  lemma fmeasurableD[dest, measurable_dest]: "A \<in> fmeasurable M \<Longrightarrow> A \<in> sets M"
    4.44    by (auto simp: fmeasurable_def)
    4.45  
    4.46 +lemma fmeasurableD2: "A \<in> fmeasurable M \<Longrightarrow> emeasure M A \<noteq> top"
    4.47 +  by (auto simp: fmeasurable_def)
    4.48 +
    4.49  lemma fmeasurableI: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> A \<in> fmeasurable M"
    4.50    by (auto simp: fmeasurable_def)
    4.51  
    4.52 @@ -1648,6 +1669,86 @@
    4.53      using assms by (intro sets.countable_INT') auto
    4.54  qed
    4.55  
    4.56 +lemma measure_Un2:
    4.57 +  "A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
    4.58 +  using measure_Union[of M A "B - A"] by (auto simp: fmeasurableD2 fmeasurable.Diff)
    4.59 +
    4.60 +lemma measure_Un3:
    4.61 +  assumes "A \<in> fmeasurable M" "B \<in> fmeasurable M"
    4.62 +  shows "measure M (A \<union> B) = measure M A + measure M B - measure M (A \<inter> B)"
    4.63 +proof -
    4.64 +  have "measure M (A \<union> B) = measure M A + measure M (B - A)"
    4.65 +    using assms by (rule measure_Un2)
    4.66 +  also have "B - A = B - (A \<inter> B)"
    4.67 +    by auto
    4.68 +  also have "measure M (B - (A \<inter> B)) = measure M B - measure M (A \<inter> B)"
    4.69 +    using assms by (intro measure_Diff) (auto simp: fmeasurable_def)
    4.70 +  finally show ?thesis
    4.71 +    by simp
    4.72 +qed
    4.73 +
    4.74 +lemma measure_Un_AE:
    4.75 +  "AE x in M. x \<notin> A \<or> x \<notin> B \<Longrightarrow> A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow>
    4.76 +  measure M (A \<union> B) = measure M A + measure M B"
    4.77 +  by (subst measure_Un2) (auto intro!: measure_eq_AE)
    4.78 +
    4.79 +lemma measure_UNION_AE:
    4.80 +  assumes I: "finite I"
    4.81 +  shows "(\<And>i. i \<in> I \<Longrightarrow> F i \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>i j. AE x in M. x \<notin> F i \<or> x \<notin> F j) I \<Longrightarrow>
    4.82 +    measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
    4.83 +  unfolding AE_pairwise[OF countable_finite, OF I]
    4.84 +  using I
    4.85 +  apply (induction I rule: finite_induct)
    4.86 +   apply simp
    4.87 +  apply (simp add: pairwise_insert)
    4.88 +  apply (subst measure_Un_AE)
    4.89 +  apply auto
    4.90 +  done
    4.91 +
    4.92 +lemma measure_UNION':
    4.93 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>i j. disjnt (F i) (F j)) I \<Longrightarrow>
    4.94 +    measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
    4.95 +  by (intro measure_UNION_AE) (auto simp: disjnt_def elim!: pairwise_mono intro!: always_eventually)
    4.96 +
    4.97 +lemma measure_Union_AE:
    4.98 +  "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> fmeasurable M) \<Longrightarrow> pairwise (\<lambda>S T. AE x in M. x \<notin> S \<or> x \<notin> T) F \<Longrightarrow>
    4.99 +    measure M (\<Union>F) = (\<Sum>S\<in>F. measure M S)"
   4.100 +  using measure_UNION_AE[of F "\<lambda>x. x" M] by simp
   4.101 +
   4.102 +lemma measure_Union':
   4.103 +  "finite F \<Longrightarrow> (\<And>S. S \<in> F \<Longrightarrow> S \<in> fmeasurable M) \<Longrightarrow> pairwise disjnt F \<Longrightarrow> measure M (\<Union>F) = (\<Sum>S\<in>F. measure M S)"
   4.104 +  using measure_UNION'[of F "\<lambda>x. x" M] by simp
   4.105 +
   4.106 +lemma measure_Un_le:
   4.107 +  assumes "A \<in> sets M" "B \<in> sets M" shows "measure M (A \<union> B) \<le> measure M A + measure M B"
   4.108 +proof cases
   4.109 +  assume "A \<in> fmeasurable M \<and> B \<in> fmeasurable M"
   4.110 +  with measure_subadditive[of A M B] assms show ?thesis
   4.111 +    by (auto simp: fmeasurableD2)
   4.112 +next
   4.113 +  assume "\<not> (A \<in> fmeasurable M \<and> B \<in> fmeasurable M)"
   4.114 +  then have "A \<union> B \<notin> fmeasurable M"
   4.115 +    using fmeasurableI2[of "A \<union> B" M A] fmeasurableI2[of "A \<union> B" M B] assms by auto
   4.116 +  with assms show ?thesis
   4.117 +    by (auto simp: fmeasurable_def measure_def less_top[symmetric])
   4.118 +qed
   4.119 +
   4.120 +lemma measure_UNION_le:
   4.121 +  "finite I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> F i \<in> sets M) \<Longrightarrow> measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
   4.122 +proof (induction I rule: finite_induct)
   4.123 +  case (insert i I)
   4.124 +  then have "measure M (\<Union>i\<in>insert i I. F i) \<le> measure M (F i) + measure M (\<Union>i\<in>I. F i)"
   4.125 +    by (auto intro!: measure_Un_le)
   4.126 +  also have "measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
   4.127 +    using insert by auto
   4.128 +  finally show ?case
   4.129 +    using insert by simp
   4.130 +qed simp
   4.131 +
   4.132 +lemma measure_Union_le:
   4.133 +  "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)"
   4.134 +  using measure_UNION_le[of F "\<lambda>x. x" M] by simp
   4.135 +
   4.136  subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
   4.137  
   4.138  locale finite_measure = sigma_finite_measure M for M +
     5.1 --- a/src/HOL/Set.thy	Thu Sep 29 13:54:57 2016 +0200
     5.2 +++ b/src/HOL/Set.thy	Thu Sep 29 18:52:34 2016 +0200
     5.3 @@ -1847,7 +1847,7 @@
     5.4  text \<open>Misc\<close>
     5.5  
     5.6  definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
     5.7 -  where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x \<noteq> y \<longrightarrow> R x y)"
     5.8 +  where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
     5.9  
    5.10  lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
    5.11    by (force simp: pairwise_def)