HOL-Analysis: prove that a starlike set is negligible (based on HOL Light proof ported by L. C. Paulson)

--- a/src/HOL/Analysis/Complete_Measure.thy	Thu Sep 29 13:54:57 2016 +0200
+++ b/src/HOL/Analysis/Complete_Measure.thy	Thu Sep 29 18:52:34 2016 +0200
@@ -794,6 +794,27 @@
 lemma (in complete_measure) complete2: "A \<subseteq> B \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> A \<in> null_sets M"
   using complete[of A B] null_sets_subset[of A B M] by simp
 
+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"
+  unfolding eventually_ae_filter by (auto intro: complete2)
+
+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)"
+  unfolding AE_iff_null_sets by (auto cong: rev_conj_cong dest: sets.sets_into_space simp: subset_eq)
+
+lemma (in complete_measure) in_sets_AE:
+  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"
+  shows "B \<in> sets M"
+proof -
+  have "(AE x in M. x \<notin> B - A \<and> x \<notin> A - B)"
+    using ae by eventually_elim auto
+  then have "B - A \<in> null_sets M" "A - B \<in> null_sets M"
+    using A B unfolding null_sets_iff_AE by (auto dest: sets.sets_into_space)
+  then have "A \<union> (B - A) - (A - B) \<in> sets M"
+    using A by blast
+  also have "A \<union> (B - A) - (A - B) = B"
+    by auto
+  finally show "B \<in> sets M" .
+qed
+
 lemma (in complete_measure) vimage_null_part_null_sets:
   assumes f: "f \<in> M \<rightarrow>\<^sub>M N" and eq: "null_sets N \<subseteq> null_sets (distr M N f)"
     and A: "A \<in> completion N"
@@ -955,6 +976,16 @@
     by simp
 qed (auto intro!: bexI[of _ S])
 
+lemma (in complete_measure) null_sets_outer:
+  "S \<in> null_sets M \<longleftrightarrow> (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T < e)"
+proof -
+  have "S \<in> null_sets M \<longleftrightarrow> (S \<in> fmeasurable M \<and> 0 = measure M S)"
+    by (auto simp: null_sets_def emeasure_eq_measure2 intro: fmeasurableI) (simp add: measure_def)
+  also have "\<dots> = (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T < e)"
+    unfolding fmeasurable_measure_inner_outer by auto
+  finally show ?thesis .
+qed
+
 lemma (in cld_measure) notin_sets_outer_measure_of_cover:
   assumes E: "E \<subseteq> space M" "E \<notin> sets M"
   shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and>

--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 29 13:54:57 2016 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 29 18:52:34 2016 +0200
@@ -959,6 +959,27 @@
 lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
   by (auto simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
 
+lemma
+  assumes \<D>: "\<D> division_of S"
+  shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
+    and content_divsion: "(\<Sum>k\<in>\<D>. measure lebesgue k) = measure lebesgue S" (is ?m)
+proof -
+  { fix d1 d2 assume *: "d1 \<in> \<D>" "d2 \<in> \<D>" "d1 \<noteq> d2"
+    then obtain a b c d where "d1 = cbox a b" "d2 = cbox c d"
+      using division_ofD(4)[OF \<D>] by blast
+    with division_ofD(5)[OF \<D> *]
+    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)"
+      by auto
+    moreover have "(cbox a b - box a b) \<union> (cbox c d - box c d) \<in> null_sets lborel"
+      by (intro null_sets.Un null_sets_cbox_Diff_box)
+    ultimately have "d1 \<inter> d2 \<in> null_sets lborel"
+      by (blast intro: null_sets_subset) }
+  then show ?l ?m
+    unfolding division_ofD(6)[OF \<D>, symmetric]
+    using division_ofD(1,4)[OF \<D>]
+    by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
+qed
+
 text \<open>This should be an abbreviation for negligible.\<close>
 lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
 proof
@@ -982,6 +1003,127 @@
   qed auto
 qed
 
+lemma starlike_negligible:
+  assumes "closed S"
+      and eq1: "\<And>c x. \<lbrakk>(a + c *\<^sub>R x) \<in> S; 0 \<le> c; a + x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
+    shows "negligible S"
+proof -
+  have "negligible (op + (-a) ` S)"
+  proof (subst negligible_on_intervals, intro allI)
+    fix u v
+    show "negligible (op + (- a) ` S \<inter> cbox u v)"
+      unfolding negligible_iff_null_sets
+      apply (rule starlike_negligible_compact)
+       apply (simp add: assms closed_translation closed_Int_compact, clarify)
+      by (metis eq1 minus_add_cancel)
+  qed
+  then show ?thesis
+    by (rule negligible_translation_rev)
+qed
+
+lemma starlike_negligible_strong:
+  assumes "closed S"
+      and star: "\<And>c x. \<lbrakk>0 \<le> c; c < 1; a+x \<in> S\<rbrakk> \<Longrightarrow> a + c *\<^sub>R x \<notin> S"
+    shows "negligible S"
+proof -
+  show ?thesis
+  proof (rule starlike_negligible [OF \<open>closed S\<close>, of a])
+    fix c x
+    assume cx: "a + c *\<^sub>R x \<in> S" "0 \<le> c" "a + x \<in> S"
+    with star have "~ (c < 1)" by auto
+    moreover have "~ (c > 1)"
+      using star [of "1/c" "c *\<^sub>R x"] cx by force
+    ultimately show "c = 1" by arith
+  qed
+qed
+
+subsection\<open>Applications\<close>
+
+lemma negligible_hyperplane:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
+proof -
+  obtain x where x: "a \<bullet> x \<noteq> b"
+    using assms
+    apply auto
+     apply (metis inner_eq_zero_iff inner_zero_right)
+    using inner_zero_right by fastforce
+  show ?thesis
+    apply (rule starlike_negligible [OF closed_hyperplane, of x])
+    using x apply (auto simp: algebra_simps)
+    done
+qed
+
+lemma negligible_lowdim:
+  fixes S :: "'N :: euclidean_space set"
+  assumes "dim S < DIM('N)"
+    shows "negligible S"
+proof -
+  obtain a where "a \<noteq> 0" and a: "span S \<subseteq> {x. a \<bullet> x = 0}"
+    using lowdim_subset_hyperplane [OF assms] by blast
+  have "negligible (span S)"
+    using \<open>a \<noteq> 0\<close> a negligible_hyperplane by (blast intro: negligible_subset)
+  then show ?thesis
+    using span_inc by (blast intro: negligible_subset)
+qed
+
+proposition negligible_convex_frontier:
+  fixes S :: "'N :: euclidean_space set"
+  assumes "convex S"
+    shows "negligible(frontier S)"
+proof -
+  have nf: "negligible(frontier S)" if "convex S" "0 \<in> S" for S :: "'N set"
+  proof -
+    obtain B where "B \<subseteq> S" and indB: "independent B"
+               and spanB: "S \<subseteq> span B" and cardB: "card B = dim S"
+      by (metis basis_exists)
+    consider "dim S < DIM('N)" | "dim S = DIM('N)"
+      using dim_subset_UNIV le_eq_less_or_eq by blast
+    then show ?thesis
+    proof cases
+      case 1
+      show ?thesis
+        by (rule negligible_subset [of "closure S"])
+           (simp_all add: Diff_subset frontier_def negligible_lowdim 1)
+    next
+      case 2
+      obtain a where a: "a \<in> interior S"
+        apply (rule interior_simplex_nonempty [OF indB])
+          apply (simp add: indB independent_finite)
+         apply (simp add: cardB 2)
+        apply (metis \<open>B \<subseteq> S\<close> \<open>0 \<in> S\<close> \<open>convex S\<close> insert_absorb insert_subset interior_mono subset_hull)
+        done
+      show ?thesis
+      proof (rule starlike_negligible_strong [where a=a])
+        fix c::real and x
+        have eq: "a + c *\<^sub>R x = (a + x) - (1 - c) *\<^sub>R ((a + x) - a)"
+          by (simp add: algebra_simps)
+        assume "0 \<le> c" "c < 1" "a + x \<in> frontier S"
+        then show "a + c *\<^sub>R x \<notin> frontier S"
+          apply (clarsimp simp: frontier_def)
+          apply (subst eq)
+          apply (rule mem_interior_closure_convex_shrink [OF \<open>convex S\<close> a, of _ "1-c"], auto)
+          done
+      qed auto
+    qed
+  qed
+  show ?thesis
+  proof (cases "S = {}")
+    case True then show ?thesis by auto
+  next
+    case False
+    then obtain a where "a \<in> S" by auto
+    show ?thesis
+      using nf [of "(\<lambda>x. -a + x) ` S"]
+      by (metis \<open>a \<in> S\<close> add.left_inverse assms convex_translation_eq frontier_translation
+                image_eqI negligible_translation_rev)
+  qed
+qed
+
+corollary negligible_sphere: "negligible (sphere a e)"
+  using frontier_cball negligible_convex_frontier convex_cball
+  by (blast intro: negligible_subset)
+
+
 lemma non_negligible_UNIV [simp]: "\<not> negligible UNIV"
   unfolding negligible_iff_null_sets by (auto simp: null_sets_def emeasure_lborel_UNIV)
 

--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 29 13:54:57 2016 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 29 18:52:34 2016 +0200
@@ -8,7 +8,7 @@
 section \<open>Lebesgue measure\<close>
 
 theory Lebesgue_Measure
-  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure
+  imports Finite_Product_Measure Bochner_Integration Caratheodory Complete_Measure Summation_Tests
 begin
 
 subsection \<open>Every right continuous and nondecreasing function gives rise to a measure\<close>
@@ -695,6 +695,19 @@
   finally show "lebesgue = density (distr lebesgue lebesgue T) (\<lambda>_. (\<Prod>j\<in>Basis. \<bar>c j\<bar>))" .
 qed
 
+lemma lebesgue_measurable_scaling[measurable]: "op *\<^sub>R x \<in> lebesgue \<rightarrow>\<^sub>M lebesgue"
+proof cases
+  assume "x = 0"
+  then have "op *\<^sub>R x = (\<lambda>x. 0::'a)"
+    by (auto simp: fun_eq_iff)
+  then show ?thesis by auto
+next
+  assume "x \<noteq> 0" then show ?thesis
+    using lebesgue_affine_measurable[of "\<lambda>_. x" 0]
+    unfolding scaleR_scaleR[symmetric] scaleR_setsum_right[symmetric] euclidean_representation
+    by (auto simp add: ac_simps)
+qed
+
 lemma
   fixes m :: real and \<delta> :: "'a::euclidean_space"
   defines "T r d x \<equiv> r *\<^sub>R x + d"
@@ -884,4 +897,93 @@
   and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
   by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
 
+lemma lmeasurable_compact: "compact S \<Longrightarrow> S \<in> lmeasurable"
+  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
+
+lemma lmeasurable_open: "bounded S \<Longrightarrow> open S \<Longrightarrow> S \<in> lmeasurable"
+  using emeasure_bounded_finite[of S] by (intro fmeasurableI) (auto simp: borel_open)
+
+lemma lmeasurable_ball: "ball a r \<in> lmeasurable"
+  by (simp add: lmeasurable_open)
+
+lemma lmeasurable_interior: "bounded S \<Longrightarrow> interior S \<in> lmeasurable"
+  by (simp add: bounded_interior lmeasurable_open)
+
+lemma null_sets_cbox_Diff_box: "cbox a b - box a b \<in> null_sets lborel"
+proof -
+  have "emeasure lborel (cbox a b - box a b) = 0"
+    by (subst emeasure_Diff) (auto simp: emeasure_lborel_cbox_eq emeasure_lborel_box_eq box_subset_cbox)
+  then have "cbox a b - box a b \<in> null_sets lborel"
+    by (auto simp: null_sets_def)
+  then show ?thesis
+    by (auto dest!: AE_not_in)
+qed
+subsection\<open> A nice lemma for negligibility proofs.\<close>
+
+lemma summable_iff_suminf_neq_top: "(\<And>n. f n \<ge> 0) \<Longrightarrow> \<not> summable f \<Longrightarrow> (\<Sum>i. ennreal (f i)) = top"
+  by (metis summable_suminf_not_top)
+
+proposition starlike_negligible_bounded_gmeasurable:
+  fixes S :: "'a :: euclidean_space set"
+  assumes S: "S \<in> sets lebesgue" and "bounded S"
+      and eq1: "\<And>c x. \<lbrakk>(c *\<^sub>R x) \<in> S; 0 \<le> c; x \<in> S\<rbrakk> \<Longrightarrow> c = 1"
+    shows "S \<in> null_sets lebesgue"
+proof -
+  obtain M where "0 < M" "S \<subseteq> ball 0 M"
+    using \<open>bounded S\<close> by (auto dest: bounded_subset_ballD)
+
+  let ?f = "\<lambda>n. root DIM('a) (Suc n)"
+
+  have vimage_eq_image: "op *\<^sub>R (?f n) -` S = op *\<^sub>R (1 / ?f n) ` S" for n
+    apply safe
+    subgoal for x by (rule image_eqI[of _ _ "?f n *\<^sub>R x"]) auto
+    subgoal by auto
+    done
+
+  have eq: "(1 / ?f n) ^ DIM('a) = 1 / Suc n" for n
+    by (simp add: field_simps)
+
+  { fix n x assume x: "root DIM('a) (1 + real n) *\<^sub>R x \<in> S"
+    have "1 * norm x \<le> root DIM('a) (1 + real n) * norm x"
+      by (rule mult_mono) auto
+    also have "\<dots> < M"
+      using x \<open>S \<subseteq> ball 0 M\<close> by auto
+    finally have "norm x < M" by simp }
+  note less_M = this
+
+  have "(\<Sum>n. ennreal (1 / Suc n)) = top"
+    using not_summable_harmonic[where 'a=real] summable_Suc_iff[where f="\<lambda>n. 1 / (real n)"]
+    by (intro summable_iff_suminf_neq_top) (auto simp add: inverse_eq_divide)
+  then have "top * emeasure lebesgue S = (\<Sum>n. (1 / ?f n)^DIM('a) * emeasure lebesgue S)"
+    unfolding ennreal_suminf_multc eq by simp
+  also have "\<dots> = (\<Sum>n. emeasure lebesgue (op *\<^sub>R (?f n) -` S))"
+    unfolding vimage_eq_image using emeasure_lebesgue_affine[of "1 / ?f n" 0 S for n] by simp
+  also have "\<dots> = emeasure lebesgue (\<Union>n. op *\<^sub>R (?f n) -` S)"
+  proof (intro suminf_emeasure)
+    show "disjoint_family (\<lambda>n. op *\<^sub>R (?f n) -` S)"
+      unfolding disjoint_family_on_def
+    proof safe
+      fix m n :: nat and x assume "m \<noteq> n" "?f m *\<^sub>R x \<in> S" "?f n *\<^sub>R x \<in> S"
+      with eq1[of "?f m / ?f n" "?f n *\<^sub>R x"] show "x \<in> {}"
+        by auto
+    qed
+    have "op *\<^sub>R (?f i) -` S \<in> sets lebesgue" for i
+      using measurable_sets[OF lebesgue_measurable_scaling[of "?f i"] S] by auto
+    then show "range (\<lambda>i. op *\<^sub>R (?f i) -` S) \<subseteq> sets lebesgue"
+      by auto
+  qed
+  also have "\<dots> \<le> emeasure lebesgue (ball 0 M :: 'a set)"
+    using less_M by (intro emeasure_mono) auto
+  also have "\<dots> < top"
+    using lmeasurable_ball by (auto simp: fmeasurable_def)
+  finally have "emeasure lebesgue S = 0"
+    by (simp add: ennreal_top_mult split: if_split_asm)
+  then show "S \<in> null_sets lebesgue"
+    unfolding null_sets_def using \<open>S \<in> sets lebesgue\<close> by auto
+qed
+
+corollary starlike_negligible_compact:
+  "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"
+  using starlike_negligible_bounded_gmeasurable[of S] by (auto simp: compact_eq_bounded_closed)
+
 end

--- a/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 13:54:57 2016 +0200
+++ b/src/HOL/Analysis/Measure_Space.thy	Thu Sep 29 18:52:34 2016 +0200
@@ -1127,6 +1127,12 @@
     unfolding eventually_ae_filter by auto
 qed auto
 
+lemma pairwise_alt: "pairwise R S \<longleftrightarrow> (\<forall>x\<in>S. \<forall>y\<in>S-{x}. R x y)"
+  by (auto simp add: pairwise_def)
+
+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)"
+  unfolding pairwise_alt by (simp add: AE_ball_countable)
+
 lemma AE_discrete_difference:
   assumes X: "countable X"
   assumes null: "\<And>x. x \<in> X \<Longrightarrow> emeasure M {x} = 0"
@@ -1453,6 +1459,12 @@
   by (simp add: enn2real_def plus_ennreal.rep_eq real_of_ereal_add less_top
            del: real_of_ereal_enn2ereal)
 
+lemma measure_eq_AE:
+  assumes iff: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B"
+  assumes A: "A \<in> sets M" and B: "B \<in> sets M"
+  shows "measure M A = measure M B"
+  using assms emeasure_eq_AE[OF assms] by (simp add: measure_def)
+
 lemma measure_Union:
   "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>
     measure M (A \<union> B) = measure M A + measure M B"
@@ -1554,6 +1566,12 @@
     done
 qed
 
+lemma measure_Un_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A \<union> B) = measure M A"
+  by (simp add: measure_def emeasure_Un_null_set)
+
+lemma measure_Diff_null_set: "A \<in> sets M \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> measure M (A - B) = measure M A"
+  by (simp add: measure_def emeasure_Diff_null_set)
+
 lemma measure_eq_setsum_singleton:
   "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>
     measure M S = (\<Sum>x\<in>S. measure M {x})"
@@ -1595,6 +1613,9 @@
 lemma fmeasurableD[dest, measurable_dest]: "A \<in> fmeasurable M \<Longrightarrow> A \<in> sets M"
   by (auto simp: fmeasurable_def)
 
+lemma fmeasurableD2: "A \<in> fmeasurable M \<Longrightarrow> emeasure M A \<noteq> top"
+  by (auto simp: fmeasurable_def)
+
 lemma fmeasurableI: "A \<in> sets M \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> A \<in> fmeasurable M"
   by (auto simp: fmeasurable_def)
 
@@ -1648,6 +1669,86 @@
     using assms by (intro sets.countable_INT') auto
 qed
 
+lemma measure_Un2:
+  "A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow> measure M (A \<union> B) = measure M A + measure M (B - A)"
+  using measure_Union[of M A "B - A"] by (auto simp: fmeasurableD2 fmeasurable.Diff)
+
+lemma measure_Un3:
+  assumes "A \<in> fmeasurable M" "B \<in> fmeasurable M"
+  shows "measure M (A \<union> B) = measure M A + measure M B - measure M (A \<inter> B)"
+proof -
+  have "measure M (A \<union> B) = measure M A + measure M (B - A)"
+    using assms by (rule measure_Un2)
+  also have "B - A = B - (A \<inter> B)"
+    by auto
+  also have "measure M (B - (A \<inter> B)) = measure M B - measure M (A \<inter> B)"
+    using assms by (intro measure_Diff) (auto simp: fmeasurable_def)
+  finally show ?thesis
+    by simp
+qed
+
+lemma measure_Un_AE:
+  "AE x in M. x \<notin> A \<or> x \<notin> B \<Longrightarrow> A \<in> fmeasurable M \<Longrightarrow> B \<in> fmeasurable M \<Longrightarrow>
+  measure M (A \<union> B) = measure M A + measure M B"
+  by (subst measure_Un2) (auto intro!: measure_eq_AE)
+
+lemma measure_UNION_AE:
+  assumes I: "finite I"
+  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>
+    measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
+  unfolding AE_pairwise[OF countable_finite, OF I]
+  using I
+  apply (induction I rule: finite_induct)
+   apply simp
+  apply (simp add: pairwise_insert)
+  apply (subst measure_Un_AE)
+  apply auto
+  done
+
+lemma measure_UNION':
+  "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>
+    measure M (\<Union>i\<in>I. F i) = (\<Sum>i\<in>I. measure M (F i))"
+  by (intro measure_UNION_AE) (auto simp: disjnt_def elim!: pairwise_mono intro!: always_eventually)
+
+lemma measure_Union_AE:
+  "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>
+    measure M (\<Union>F) = (\<Sum>S\<in>F. measure M S)"
+  using measure_UNION_AE[of F "\<lambda>x. x" M] by simp
+
+lemma measure_Union':
+  "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)"
+  using measure_UNION'[of F "\<lambda>x. x" M] by simp
+
+lemma measure_Un_le:
+  assumes "A \<in> sets M" "B \<in> sets M" shows "measure M (A \<union> B) \<le> measure M A + measure M B"
+proof cases
+  assume "A \<in> fmeasurable M \<and> B \<in> fmeasurable M"
+  with measure_subadditive[of A M B] assms show ?thesis
+    by (auto simp: fmeasurableD2)
+next
+  assume "\<not> (A \<in> fmeasurable M \<and> B \<in> fmeasurable M)"
+  then have "A \<union> B \<notin> fmeasurable M"
+    using fmeasurableI2[of "A \<union> B" M A] fmeasurableI2[of "A \<union> B" M B] assms by auto
+  with assms show ?thesis
+    by (auto simp: fmeasurable_def measure_def less_top[symmetric])
+qed
+
+lemma measure_UNION_le:
+  "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))"
+proof (induction I rule: finite_induct)
+  case (insert i I)
+  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)"
+    by (auto intro!: measure_Un_le)
+  also have "measure M (\<Union>i\<in>I. F i) \<le> (\<Sum>i\<in>I. measure M (F i))"
+    using insert by auto
+  finally show ?case
+    using insert by simp
+qed simp
+
+lemma measure_Union_le:
+  "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)"
+  using measure_UNION_le[of F "\<lambda>x. x" M] by simp
+
 subsection \<open>Measure spaces with @{term "emeasure M (space M) < \<infinity>"}\<close>
 
 locale finite_measure = sigma_finite_measure M for M +

--- a/src/HOL/Set.thy	Thu Sep 29 13:54:57 2016 +0200
+++ b/src/HOL/Set.thy	Thu Sep 29 18:52:34 2016 +0200
@@ -1847,7 +1847,7 @@
 text \<open>Misc\<close>
 
 definition pairwise :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> bool"
-  where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y\<in> S. x \<noteq> y \<longrightarrow> R x y)"
+  where "pairwise R S \<longleftrightarrow> (\<forall>x \<in> S. \<forall>y \<in> S. x \<noteq> y \<longrightarrow> R x y)"
 
 lemma pairwise_subset: "pairwise P S \<Longrightarrow> T \<subseteq> S \<Longrightarrow> pairwise P T"
   by (force simp: pairwise_def)