# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523887246 -3600
# Node ID 706f86afff43106d60ff94576b9b55aa7ddc3c15
# Parent  01c6514120811178aa6e307768cbfd4a1ca1e3e7
more results about measure and negligibility

diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 16 05:34:25 2018 +0000
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 16 15:00:46 2018 +0100
@@ -1116,6 +1116,36 @@
     by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
 qed
 
+lemma has_measure_limit:
+  assumes "S \<in> lmeasurable" "e > 0"
+  obtains B where "B > 0"
+    "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> \<bar>measure lebesgue (S \<inter> cbox a b) - measure lebesgue S\<bar> < e"
+  using assms unfolding lmeasurable_iff_has_integral has_integral_alt'
+  by (force simp: integral_indicator integrable_on_indicator)
+
+lemma lmeasurable_iff_indicator_has_integral:
+  fixes S :: "'a::euclidean_space set"
+  shows "S \<in> lmeasurable \<and> m = measure lebesgue S \<longleftrightarrow> (indicat_real S has_integral m) UNIV"
+  by (metis has_integral_iff lmeasurable_iff_has_integral measurable_integrable)
+
+lemma has_measure_limit_iff:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
+  shows "S \<in> lmeasurable \<and> m = measure lebesgue S \<longleftrightarrow>
+          (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
+            (S \<inter> cbox a b) \<in> lmeasurable \<and> \<bar>measure lebesgue (S \<inter> cbox a b) - m\<bar> < e)" (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox)
+next
+  assume RHS [rule_format]: ?rhs
+  show ?lhs
+    apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m])
+    using RHS
+    by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator)
+qed
+
+subsection\<open>Applications to Negligibility\<close>
+
 lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
 proof
   assume "negligible S"
@@ -1172,8 +1202,6 @@
   qed
 qed
 
-subsection\<open>Applications to Negligibility\<close>
-
 lemma negligible_hyperplane:
   assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
 proof -
@@ -1258,7 +1286,6 @@
   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)
 
@@ -1268,6 +1295,36 @@
                   not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
             intro: eq_refl antisym less_imp_le)
 
+proposition open_not_negligible:
+  assumes "open S" "S \<noteq> {}"
+  shows "\<not> negligible S"
+proof
+  assume neg: "negligible S"
+  obtain a where "a \<in> S"
+    using \<open>S \<noteq> {}\<close> by blast
+  then obtain e where "e > 0" "cball a e \<subseteq> S"
+    using \<open>open S\<close> open_contains_cball_eq by blast
+  let ?p = "a - (e / DIM('a)) *\<^sub>R One" let ?q = "a + (e / DIM('a)) *\<^sub>R One"
+  have "cbox ?p ?q \<subseteq> cball a e"
+  proof (clarsimp simp: mem_box dist_norm)
+    fix x
+    assume "\<forall>i\<in>Basis. ?p \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> ?q \<bullet> i"
+    then have ax: "\<bar>(a - x) \<bullet> i\<bar> \<le> e / real DIM('a)" if "i \<in> Basis" for i
+      using that by (auto simp: algebra_simps)
+    have "norm (a - x) \<le> (\<Sum>i\<in>Basis. \<bar>(a - x) \<bullet> i\<bar>)"
+      by (rule norm_le_l1)
+    also have "\<dots> \<le> DIM('a) * (e / real DIM('a))"
+      by (intro sum_bounded_above ax)
+    also have "\<dots> = e"
+      by simp
+    finally show "norm (a - x) \<le> e" .
+  qed
+  then have "negligible (cbox ?p ?q)"
+    by (meson \<open>cball a e \<subseteq> S\<close> neg negligible_subset)
+  with \<open>e > 0\<close> show False
+    by (simp add: negligible_interval box_eq_empty algebra_simps divide_simps mult_le_0_iff)
+qed
+
 lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
   by (auto simp: measure_def null_sets_def)
 
@@ -1337,7 +1394,36 @@
     by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0)
 qed
 
-text\<open>Negligibility of image under non-injective linear map\<close>
+lemma measure_closure:
+  assumes "bounded S" and neg: "negligible (frontier S)"
+  shows "measure lebesgue (closure S) = measure lebesgue S"
+proof -
+  have "measure lebesgue (frontier S) = 0"
+    by (metis neg negligible_imp_measure0)
+  then show ?thesis
+    by (metis assms lmeasurable_iff_integrable_on eq_iff_diff_eq_0 has_integral_interior integrable_on_def integral_unique lmeasurable_interior lmeasure_integral measure_frontier)
+qed
+
+lemma measure_interior:
+   "\<lbrakk>bounded S; negligible(frontier S)\<rbrakk> \<Longrightarrow> measure lebesgue (interior S) = measure lebesgue S"
+  using measure_closure measure_frontier negligible_imp_measure0 by fastforce
+
+lemma measurable_Jordan:
+  assumes "bounded S" and neg: "negligible (frontier S)"
+  shows "S \<in> lmeasurable"
+proof -
+  have "closure S \<in> lmeasurable"
+    by (metis lmeasurable_closure \<open>bounded S\<close>)
+  moreover have "interior S \<in> lmeasurable"
+    by (simp add: lmeasurable_interior \<open>bounded S\<close>)
+  moreover have "interior S \<subseteq> S"
+    by (simp add: interior_subset)
+  ultimately show ?thesis
+    using assms by (metis (full_types) closure_subset completion.complete_sets_sandwich_fmeasurable measure_closure measure_interior)
+qed
+
+subsection\<open>Negligibility of image under non-injective linear map\<close>
+
 lemma negligible_Union_nat:
   assumes "\<And>n::nat. negligible(S n)"
   shows "negligible(\<Union>n. S n)"
@@ -1362,6 +1448,59 @@
     using * by (simp add: negligible_UNIV has_integral_iff)
 qed
 
+
+lemma negligible_linear_singular_image:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "linear f" "\<not> inj f"
+  shows "negligible (f ` S)"
+proof -
+  obtain a where "a \<noteq> 0" "\<And>S. f ` S \<subseteq> {x. a \<bullet> x = 0}"
+    using assms linear_singular_image_hyperplane by blast
+  then show "negligible (f ` S)"
+    by (metis negligible_hyperplane negligible_subset)
+qed
+
+lemma measure_negligible_finite_Union:
+  assumes "finite \<F>"
+    and meas: "\<And>S. S \<in> \<F> \<Longrightarrow> S \<in> lmeasurable"
+    and djointish: "pairwise (\<lambda>S T. negligible (S \<inter> T)) \<F>"
+  shows "measure lebesgue (\<Union>\<F>) = (\<Sum>S\<in>\<F>. measure lebesgue S)"
+  using assms
+proof (induction)
+  case empty
+  then show ?case
+    by auto
+next
+  case (insert S \<F>)
+  then have "S \<in> lmeasurable" "\<Union>\<F> \<in> lmeasurable" "pairwise (\<lambda>S T. negligible (S \<inter> T)) \<F>"
+    by (simp_all add: fmeasurable.finite_Union insert.hyps(1) insert.prems(1) pairwise_insert subsetI)
+  then show ?case
+  proof (simp add: measure_Un3 insert)
+    have *: "\<And>T. T \<in> (\<inter>) S ` \<F> \<Longrightarrow> negligible T"
+      using insert by (force simp: pairwise_def)
+    have "negligible(S \<inter> \<Union>\<F>)"
+      unfolding Int_Union
+      by (rule negligible_Union) (simp_all add: * insert.hyps(1))
+    then show "measure lebesgue (S \<inter> \<Union>\<F>) = 0"
+      using negligible_imp_measure0 by blast
+  qed
+qed
+
+lemma measure_negligible_finite_Union_image:
+  assumes "finite S"
+    and meas: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> lmeasurable"
+    and djointish: "pairwise (\<lambda>x y. negligible (f x \<inter> f y)) S"
+  shows "measure lebesgue (\<Union>(f ` S)) = (\<Sum>x\<in>S. measure lebesgue (f x))"
+proof -
+  have "measure lebesgue (\<Union>(f ` S)) = sum (measure lebesgue) (f ` S)"
+    using assms by (auto simp: pairwise_mono pairwise_image intro: measure_negligible_finite_Union)
+  also have "\<dots> = sum (measure lebesgue \<circ> f) S"
+    using djointish [unfolded pairwise_def] by (metis inf.idem negligible_imp_measure0 sum.reindex_nontrivial [OF \<open>finite S\<close>])
+  also have "\<dots> = (\<Sum>x\<in>S. measure lebesgue (f x))"
+    by simp
+  finally show ?thesis .
+qed
+
 subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
 
 text\<open>The bound will be eliminated by a sort of onion argument\<close>
@@ -1596,12 +1735,10 @@
       by (auto simp: fbx_def)
     have 2: "I' \<subseteq> \<D> \<Longrightarrow> finite I' \<Longrightarrow> measure lebesgue (\<Union>D\<in>I'. fbx D) \<le> e/2" for I'
       by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def)
-    have 3: "0 \<le> e/2"
-      using \<open>0<e\<close> by auto
     show "(\<Union>D\<in>\<D>. fbx D) \<in> lmeasurable"
-      by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
+      by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2])
     have "measure lebesgue (\<Union>D\<in>\<D>. fbx D) \<le> e/2"
-      by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
+      by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2])
     then show "measure lebesgue (\<Union>D\<in>\<D>. fbx D) < e"
       using \<open>0 < e\<close> by linarith
   qed
@@ -1722,6 +1859,134 @@
     done
 qed
 
+subsection\<open>Measurability of countable unions and intersections of various kinds.\<close>
+
+lemma
+  assumes S: "\<And>n. S n \<in> lmeasurable"
+    and leB: "\<And>n. measure lebesgue (S n) \<le> B"
+    and nest: "\<And>n. S n \<subseteq> S(Suc n)"
+  shows measurable_nested_Union: "(\<Union>n. S n) \<in> lmeasurable"
+  and measure_nested_Union:  "(\<lambda>n. measure lebesgue (S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. S n)" (is ?Lim)
+proof -
+  have 1: "\<And>n. (indicat_real (S n)) integrable_on UNIV"
+    using S measurable_integrable by blast
+  have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
+    by (simp add: indicator_leI nest rev_subsetD)
+  have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (UNION UNIV S) x)"
+    apply (rule Lim_eventually)
+    apply (simp add: indicator_def)
+    by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
+  have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
+    using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
+  have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
+    apply (simp add: lmeasure_integral_UNIV S cong: conj_cong)
+    apply (simp add: measurable_integrable)
+    apply (rule monotone_convergence_increasing [OF 1 2 3 4])
+    done
+  then show "(\<Union>n. S n) \<in> lmeasurable" "?Lim"
+    by auto
+qed
+
+lemma
+  assumes S: "\<And>n. S n \<in> lmeasurable"
+    and djointish: "pairwise (\<lambda>m n. negligible (S m \<inter> S n)) UNIV"
+    and leB: "\<And>n. (\<Sum>k\<le>n. measure lebesgue (S k)) \<le> B"
+  shows measurable_countable_negligible_Union: "(\<Union>n. S n) \<in> lmeasurable"
+  and   measure_countable_negligible_Union:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
+proof -
+  have 1: "UNION {..n} S \<in> lmeasurable" for n
+    using S by blast
+  have 2: "measure lebesgue (UNION {..n} S) \<le> B" for n
+  proof -
+    have "measure lebesgue (UNION {..n} S) \<le> (\<Sum>k\<le>n. measure lebesgue (S k))"
+      by (simp add: S fmeasurableD measure_UNION_le)
+    with leB show ?thesis
+      using order_trans by blast
+  qed
+  have 3: "\<And>n. UNION {..n} S \<subseteq> UNION {..Suc n} S"
+    by (simp add: SUP_subset_mono)
+  have eqS: "(\<Union>n. S n) = (\<Union>n. UNION {..n} S)"
+    using atLeastAtMost_iff by blast
+  also have "(\<Union>n. UNION {..n} S) \<in> lmeasurable"
+    by (intro measurable_nested_Union [OF 1 2] 3)
+  finally show "(\<Union>n. S n) \<in> lmeasurable" .
+  have eqm: "(\<Sum>i\<le>n. measure lebesgue (S i)) = measure lebesgue (UNION {..n} S)" for n
+    using assms by (simp add: measure_negligible_finite_Union_image pairwise_mono)
+  have "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. UNION {..n} S)"
+    by (simp add: sums_def' eqm atLeast0AtMost) (intro measure_nested_Union [OF 1 2] 3)
+  then show ?Sums
+    by (simp add: eqS)
+qed
+
+lemma negligible_countable_Union [intro]:
+  assumes "countable \<F>" and meas: "\<And>S. S \<in> \<F> \<Longrightarrow> negligible S"
+  shows "negligible (\<Union>\<F>)"
+proof (cases "\<F> = {}")
+  case False
+  then show ?thesis
+    by (metis from_nat_into range_from_nat_into assms negligible_Union_nat)
+qed simp
+
+lemma
+  assumes S: "\<And>n. (S n) \<in> lmeasurable"
+    and djointish: "pairwise (\<lambda>m n. negligible (S m \<inter> S n)) UNIV"
+    and bo: "bounded (\<Union>n. S n)"
+  shows measurable_countable_negligible_Union_bounded: "(\<Union>n. S n) \<in> lmeasurable"
+  and   measure_countable_negligible_Union_bounded:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
+proof -
+  obtain a b where ab: "(\<Union>n. S n) \<subseteq> cbox a b"
+    using bo bounded_subset_cbox by blast
+  then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
+  proof -
+    have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
+      using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
+      by (metis S finite_atMost subset_UNIV)
+    also have "\<dots> \<le> measure lebesgue (cbox a b)"
+      apply (rule measure_mono_fmeasurable)
+      using ab S by force+
+    finally show ?thesis .
+  qed
+  show "(\<Union>n. S n) \<in> lmeasurable"
+    by (rule measurable_countable_negligible_Union [OF S djointish B])
+  show ?Sums
+    by (rule measure_countable_negligible_Union [OF S djointish B])
+qed
+
+lemma measure_countable_Union_approachable:
+  assumes "countable \<D>" "e > 0" and measD: "\<And>d. d \<in> \<D> \<Longrightarrow> d \<in> lmeasurable"
+      and B: "\<And>D'. \<lbrakk>D' \<subseteq> \<D>; finite D'\<rbrakk> \<Longrightarrow> measure lebesgue (\<Union>D') \<le> B"
+    obtains D' where "D' \<subseteq> \<D>" "finite D'" "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (\<Union>D')"
+proof (cases "\<D> = {}")
+  case True
+  then show ?thesis
+    by (simp add: \<open>e > 0\<close> that)
+next
+  case False
+  let ?S = "\<lambda>n. \<Union>k \<le> n. from_nat_into \<D> k"
+  have "(\<lambda>n. measure lebesgue (?S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. ?S n)"
+  proof (rule measure_nested_Union)
+    show "?S n \<in> lmeasurable" for n
+      by (simp add: False fmeasurable.finite_UN from_nat_into measD)
+    show "measure lebesgue (?S n) \<le> B" for n
+      by (metis (mono_tags, lifting) B False finite_atMost finite_imageI from_nat_into image_iff subsetI)
+    show "?S n \<subseteq> ?S (Suc n)" for n
+      by force
+  qed
+  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> dist (measure lebesgue (?S n)) (measure lebesgue (\<Union>n. ?S n)) < e"
+    using metric_LIMSEQ_D \<open>e > 0\<close> by blast
+  show ?thesis
+  proof
+    show "from_nat_into \<D> ` {..N} \<subseteq> \<D>"
+      by (auto simp: False from_nat_into)
+    have eq: "(\<Union>n. \<Union>k\<le>n. from_nat_into \<D> k) = (\<Union>\<D>)"
+      using \<open>countable \<D>\<close> False
+      by (auto intro: from_nat_into dest: from_nat_into_surj [OF \<open>countable \<D>\<close>])
+    show "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (UNION {..N} (from_nat_into \<D>))"
+      using N [OF order_refl]
+      by (auto simp: eq algebra_simps dist_norm)
+  qed auto
+qed
+
 subsection\<open>Integral bounds\<close>
 
 lemma set_integral_norm_bound:
diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Apr 16 05:34:25 2018 +0000
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Apr 16 15:00:46 2018 +0100
@@ -978,8 +978,24 @@
   and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
   by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
 
+lemma fmeasurable_compact: "compact S \<Longrightarrow> S \<in> fmeasurable lborel"
+  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
+
 lemma lmeasurable_compact: "compact S \<Longrightarrow> S \<in> lmeasurable"
-  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
+  using fmeasurable_compact by (force simp: fmeasurable_def)
+
+lemma measure_frontier:
+   "bounded S \<Longrightarrow> measure lebesgue (frontier S) = measure lebesgue (closure S) - measure lebesgue (interior S)"
+  using closure_subset interior_subset
+  by (auto simp: frontier_def fmeasurable_compact intro!: measurable_measure_Diff)
+
+lemma lmeasurable_closure:
+   "bounded S \<Longrightarrow> closure S \<in> lmeasurable"
+  by (simp add: lmeasurable_compact)
+
+lemma lmeasurable_frontier:
+   "bounded S \<Longrightarrow> frontier S \<in> lmeasurable"
+  by (simp add: compact_frontier_bounded lmeasurable_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)
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\<open>Measurable sets formed by unions and intersections\<close>
+
 lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
   using fmeasurableI2[of A M "A - B"] by auto
 
@@ -1882,15 +1884,20 @@
   "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
 
+text\<open>Version for indexed union over a countable set\<close>
 lemma
   assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> fmeasurable M"
-    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"
+    and bound: "\<And>I'. I' \<subseteq> I \<Longrightarrow> finite I' \<Longrightarrow> measure M (\<Union>i\<in>I'. A i) \<le> B"
   shows fmeasurable_UN_bound: "(\<Union>i\<in>I. A i) \<in> fmeasurable M" (is ?fm)
     and measure_UN_bound: "measure M (\<Union>i\<in>I. A i) \<le> B" (is ?m)
 proof -
+  have "B \<ge> 0"
+    using bound by force
   have "?fm \<and> ?m"
   proof cases
-    assume "I = {}" with \<open>0 \<le> B\<close> show ?thesis by simp
+    assume "I = {}"
+    with \<open>B \<ge> 0\<close> show ?thesis
+      by simp
   next
     assume "I \<noteq> {}"
     have "(\<Union>i\<in>I. A i) = (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))"
@@ -1918,6 +1925,58 @@
   then show ?fm ?m by auto
 qed
 
+text\<open>Version for big union of a countable set\<close>
+lemma
+  assumes "countable \<D>"
+    and meas: "\<And>D. D \<in> \<D> \<Longrightarrow> D \<in> fmeasurable M"
+    and bound:  "\<And>\<E>. \<lbrakk>\<E> \<subseteq> \<D>; finite \<E>\<rbrakk> \<Longrightarrow> measure M (\<Union>\<E>) \<le> B"
+ shows fmeasurable_Union_bound: "\<Union>\<D> \<in> fmeasurable M"  (is ?fm)
+    and measure_Union_bound: "measure M (\<Union>\<D>) \<le> B"     (is ?m)
+proof -
+  have "B \<ge> 0"
+    using bound by force
+  have "?fm \<and> ?m"
+  proof (cases "\<D> = {}")
+    case True
+    with \<open>B \<ge> 0\<close> show ?thesis
+      by auto
+  next
+    case False
+    then obtain D :: "nat \<Rightarrow> 'a set" where D: "\<D> = range D"
+      using \<open>countable \<D>\<close> uncountable_def by force
+      have 1: "\<And>i. D i \<in> fmeasurable M"
+        by (simp add: D meas)
+      have 2: "\<And>I'. finite I' \<Longrightarrow> measure M (\<Union>x\<in>I'. D x) \<le> 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\<open>Version for indexed union over the type of naturals\<close>
+lemma
+  fixes S :: "nat \<Rightarrow> 'a set"
+  assumes S: "\<And>i. S i \<in> fmeasurable M" and B: "\<And>n. measure M (\<Union>i\<le>n. S i) \<le> B"
+  shows fmeasurable_countable_Union: "(\<Union>i. S i) \<in> fmeasurable M"
+    and measure_countable_Union_le: "measure M (\<Union>i. S i) \<le> B"
+proof -
+  have mB: "measure M (\<Union>i\<in>I. S i) \<le> B" if "finite I" for I
+  proof -
+    have "(\<Union>i\<in>I. S i) \<subseteq> (\<Union>i\<le>Max I. S i)"
+      using Max_ge that by force
+    then have "measure M (\<Union>i\<in>I. S i) \<le> measure M (\<Union>i \<le> Max I. S i)"
+      by (rule measure_mono_fmeasurable) (use S in \<open>blast+\<close>)
+    then show ?thesis
+      using B order_trans by blast
+  qed
+  show "(\<Union>i. S i) \<in> fmeasurable M"
+    by (auto intro: fmeasurable_UN_bound [OF _ S mB])
+  show "measure M (\<Union>n. S n) \<le> B"
+    by (auto intro: measure_UN_bound [OF _ S mB])
+qed
+
 lemma measure_diff_le_measure_setdiff:
   assumes "S \<in> fmeasurable M" "T \<in> fmeasurable M"
   shows "measure M S - measure M T \<le> measure M (S - T)"
diff -r 01c651412081 -r 706f86afff43 src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Mon Apr 16 05:34:25 2018 +0000
+++ b/src/HOL/Analysis/Starlike.thy	Mon Apr 16 15:00:46 2018 +0100
@@ -8421,6 +8421,83 @@
   apply (simp add: adjoint_works assms(1) inner_commute)
   by (metis adjoint_works all_zero_iff assms(1) inner_commute)
 
+subsection\<open> A non-injective linear function maps into a hyperplane.\<close>
+
+lemma linear_surj_adj_imp_inj:
+  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+  assumes "linear f" "surj (adjoint f)"
+  shows "inj f"
+proof -
+  have "\<exists>x. y = adjoint f x" for y
+    using assms by (simp add: surjD)
+  then show "inj f"
+    using assms unfolding inj_on_def image_def
+    by (metis (no_types) adjoint_works euclidean_eqI)
+qed
+
+(*http://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map*)
+lemma surj_adjoint_iff_inj [simp]:
+  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+  assumes "linear f"
+  shows  "surj (adjoint f) \<longleftrightarrow> inj f"
+proof
+  assume "surj (adjoint f)"
+  then show "inj f"
+    by (simp add: assms linear_surj_adj_imp_inj)
+next
+  assume "inj f"
+  have "f -` {0} = {0}"
+    using assms \<open>inj f\<close> linear_0 linear_injective_0 by fastforce
+  moreover have "f -` {0} = range (adjoint f)\<^sup>\<bottom>"
+    by (intro ker_orthogonal_comp_adjoint assms)
+  ultimately have "range (adjoint f)\<^sup>\<bottom>\<^sup>\<bottom> = UNIV"
+    by (metis orthogonal_comp_null)
+  then show "surj (adjoint f)"
+    by (simp add: adjoint_linear \<open>linear f\<close> subspace_linear_image orthogonal_comp_self)
+qed
+
+lemma inj_adjoint_iff_surj [simp]:
+  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
+  assumes "linear f"
+  shows  "inj (adjoint f) \<longleftrightarrow> surj f"
+proof
+  assume "inj (adjoint f)"
+  have "(adjoint f) -` {0} = {0}"
+    by (metis \<open>inj (adjoint f)\<close> adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV)
+  then have "(range(f))\<^sup>\<bottom> = {0}"
+    by (metis (no_types, hide_lams) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero)
+  then show "surj f"
+    by (metis \<open>inj (adjoint f)\<close> adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj)
+next
+  assume "surj f"
+  then have "range f = (adjoint f -` {0})\<^sup>\<bottom>"
+    by (simp add: adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint)
+  then have "{0} = adjoint f -` {0}"
+    using \<open>surj f\<close> adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint by force
+  then show "inj (adjoint f)"
+    by (simp add: \<open>surj f\<close> adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj)
+qed
+
+proposition linear_singular_into_hyperplane:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "linear f"
+  shows "\<not> inj f \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> (\<forall>x. a \<bullet> f x = 0))" (is "_ = ?rhs")
+proof
+  assume "\<not>inj f"
+  then show ?rhs
+    using all_zero_iff
+    by (metis (no_types, hide_lams) adjoint_clauses(2) adjoint_linear assms linear_injective_0 linear_injective_imp_surjective linear_surj_adj_imp_inj)
+next
+  assume ?rhs
+  then show "\<not>inj f"
+    by (metis assms linear_injective_isomorphism all_zero_iff)
+qed
+
+lemma linear_singular_image_hyperplane:
+  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
+  assumes "linear f" "\<not>inj f"
+  obtains a where "a \<noteq> 0" "\<And>S. f ` S \<subseteq> {x. a \<bullet> x = 0}"
+  using assms by (fastforce simp add: linear_singular_into_hyperplane)
 
 end