more results about measure and negligibility
authorpaulson <lp15@cam.ac.uk>
Mon Apr 16 15:00:46 2018 +0100 (18 months ago)
changeset 67989706f86afff43
parent 67988 01c651412081
child 67990 c0ebecf6e3eb
more results about measure and negligibility
src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
src/HOL/Analysis/Lebesgue_Measure.thy
src/HOL/Analysis/Measure_Space.thy
src/HOL/Analysis/Starlike.thy
     1.1 --- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 16 05:34:25 2018 +0000
     1.2 +++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Mon Apr 16 15:00:46 2018 +0100
     1.3 @@ -1116,6 +1116,36 @@
     1.4      by (auto intro!: measure_Union_AE[symmetric] simp: completion.AE_iff_null_sets Int_def[symmetric] pairwise_def null_sets_def)
     1.5  qed
     1.6  
     1.7 +lemma has_measure_limit:
     1.8 +  assumes "S \<in> lmeasurable" "e > 0"
     1.9 +  obtains B where "B > 0"
    1.10 +    "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow> \<bar>measure lebesgue (S \<inter> cbox a b) - measure lebesgue S\<bar> < e"
    1.11 +  using assms unfolding lmeasurable_iff_has_integral has_integral_alt'
    1.12 +  by (force simp: integral_indicator integrable_on_indicator)
    1.13 +
    1.14 +lemma lmeasurable_iff_indicator_has_integral:
    1.15 +  fixes S :: "'a::euclidean_space set"
    1.16 +  shows "S \<in> lmeasurable \<and> m = measure lebesgue S \<longleftrightarrow> (indicat_real S has_integral m) UNIV"
    1.17 +  by (metis has_integral_iff lmeasurable_iff_has_integral measurable_integrable)
    1.18 +
    1.19 +lemma has_measure_limit_iff:
    1.20 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
    1.21 +  shows "S \<in> lmeasurable \<and> m = measure lebesgue S \<longleftrightarrow>
    1.22 +          (\<forall>e>0. \<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
    1.23 +            (S \<inter> cbox a b) \<in> lmeasurable \<and> \<bar>measure lebesgue (S \<inter> cbox a b) - m\<bar> < e)" (is "?lhs = ?rhs")
    1.24 +proof
    1.25 +  assume ?lhs then show ?rhs
    1.26 +    by (meson has_measure_limit fmeasurable.Int lmeasurable_cbox)
    1.27 +next
    1.28 +  assume RHS [rule_format]: ?rhs
    1.29 +  show ?lhs
    1.30 +    apply (simp add: lmeasurable_iff_indicator_has_integral has_integral' [where i=m])
    1.31 +    using RHS
    1.32 +    by (metis (full_types) integral_indicator integrable_integral integrable_on_indicator)
    1.33 +qed
    1.34 +
    1.35 +subsection\<open>Applications to Negligibility\<close>
    1.36 +
    1.37  lemma negligible_iff_null_sets: "negligible S \<longleftrightarrow> S \<in> null_sets lebesgue"
    1.38  proof
    1.39    assume "negligible S"
    1.40 @@ -1172,8 +1202,6 @@
    1.41    qed
    1.42  qed
    1.43  
    1.44 -subsection\<open>Applications to Negligibility\<close>
    1.45 -
    1.46  lemma negligible_hyperplane:
    1.47    assumes "a \<noteq> 0 \<or> b \<noteq> 0" shows "negligible {x. a \<bullet> x = b}"
    1.48  proof -
    1.49 @@ -1258,7 +1286,6 @@
    1.50    using frontier_cball negligible_convex_frontier convex_cball
    1.51    by (blast intro: negligible_subset)
    1.52  
    1.53 -
    1.54  lemma non_negligible_UNIV [simp]: "\<not> negligible UNIV"
    1.55    unfolding negligible_iff_null_sets by (auto simp: null_sets_def emeasure_lborel_UNIV)
    1.56  
    1.57 @@ -1268,6 +1295,36 @@
    1.58                    not_le emeasure_lborel_cbox_eq emeasure_lborel_box_eq
    1.59              intro: eq_refl antisym less_imp_le)
    1.60  
    1.61 +proposition open_not_negligible:
    1.62 +  assumes "open S" "S \<noteq> {}"
    1.63 +  shows "\<not> negligible S"
    1.64 +proof
    1.65 +  assume neg: "negligible S"
    1.66 +  obtain a where "a \<in> S"
    1.67 +    using \<open>S \<noteq> {}\<close> by blast
    1.68 +  then obtain e where "e > 0" "cball a e \<subseteq> S"
    1.69 +    using \<open>open S\<close> open_contains_cball_eq by blast
    1.70 +  let ?p = "a - (e / DIM('a)) *\<^sub>R One" let ?q = "a + (e / DIM('a)) *\<^sub>R One"
    1.71 +  have "cbox ?p ?q \<subseteq> cball a e"
    1.72 +  proof (clarsimp simp: mem_box dist_norm)
    1.73 +    fix x
    1.74 +    assume "\<forall>i\<in>Basis. ?p \<bullet> i \<le> x \<bullet> i \<and> x \<bullet> i \<le> ?q \<bullet> i"
    1.75 +    then have ax: "\<bar>(a - x) \<bullet> i\<bar> \<le> e / real DIM('a)" if "i \<in> Basis" for i
    1.76 +      using that by (auto simp: algebra_simps)
    1.77 +    have "norm (a - x) \<le> (\<Sum>i\<in>Basis. \<bar>(a - x) \<bullet> i\<bar>)"
    1.78 +      by (rule norm_le_l1)
    1.79 +    also have "\<dots> \<le> DIM('a) * (e / real DIM('a))"
    1.80 +      by (intro sum_bounded_above ax)
    1.81 +    also have "\<dots> = e"
    1.82 +      by simp
    1.83 +    finally show "norm (a - x) \<le> e" .
    1.84 +  qed
    1.85 +  then have "negligible (cbox ?p ?q)"
    1.86 +    by (meson \<open>cball a e \<subseteq> S\<close> neg negligible_subset)
    1.87 +  with \<open>e > 0\<close> show False
    1.88 +    by (simp add: negligible_interval box_eq_empty algebra_simps divide_simps mult_le_0_iff)
    1.89 +qed
    1.90 +
    1.91  lemma measure_eq_0_null_sets: "S \<in> null_sets M \<Longrightarrow> measure M S = 0"
    1.92    by (auto simp: measure_def null_sets_def)
    1.93  
    1.94 @@ -1337,7 +1394,36 @@
    1.95      by (metis S Un_commute add.right_neutral lmeasurable_negligible_symdiff measure_Un2 neg negligible_Un_eq negligible_imp_measure0)
    1.96  qed
    1.97  
    1.98 -text\<open>Negligibility of image under non-injective linear map\<close>
    1.99 +lemma measure_closure:
   1.100 +  assumes "bounded S" and neg: "negligible (frontier S)"
   1.101 +  shows "measure lebesgue (closure S) = measure lebesgue S"
   1.102 +proof -
   1.103 +  have "measure lebesgue (frontier S) = 0"
   1.104 +    by (metis neg negligible_imp_measure0)
   1.105 +  then show ?thesis
   1.106 +    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)
   1.107 +qed
   1.108 +
   1.109 +lemma measure_interior:
   1.110 +   "\<lbrakk>bounded S; negligible(frontier S)\<rbrakk> \<Longrightarrow> measure lebesgue (interior S) = measure lebesgue S"
   1.111 +  using measure_closure measure_frontier negligible_imp_measure0 by fastforce
   1.112 +
   1.113 +lemma measurable_Jordan:
   1.114 +  assumes "bounded S" and neg: "negligible (frontier S)"
   1.115 +  shows "S \<in> lmeasurable"
   1.116 +proof -
   1.117 +  have "closure S \<in> lmeasurable"
   1.118 +    by (metis lmeasurable_closure \<open>bounded S\<close>)
   1.119 +  moreover have "interior S \<in> lmeasurable"
   1.120 +    by (simp add: lmeasurable_interior \<open>bounded S\<close>)
   1.121 +  moreover have "interior S \<subseteq> S"
   1.122 +    by (simp add: interior_subset)
   1.123 +  ultimately show ?thesis
   1.124 +    using assms by (metis (full_types) closure_subset completion.complete_sets_sandwich_fmeasurable measure_closure measure_interior)
   1.125 +qed
   1.126 +
   1.127 +subsection\<open>Negligibility of image under non-injective linear map\<close>
   1.128 +
   1.129  lemma negligible_Union_nat:
   1.130    assumes "\<And>n::nat. negligible(S n)"
   1.131    shows "negligible(\<Union>n. S n)"
   1.132 @@ -1362,6 +1448,59 @@
   1.133      using * by (simp add: negligible_UNIV has_integral_iff)
   1.134  qed
   1.135  
   1.136 +
   1.137 +lemma negligible_linear_singular_image:
   1.138 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
   1.139 +  assumes "linear f" "\<not> inj f"
   1.140 +  shows "negligible (f ` S)"
   1.141 +proof -
   1.142 +  obtain a where "a \<noteq> 0" "\<And>S. f ` S \<subseteq> {x. a \<bullet> x = 0}"
   1.143 +    using assms linear_singular_image_hyperplane by blast
   1.144 +  then show "negligible (f ` S)"
   1.145 +    by (metis negligible_hyperplane negligible_subset)
   1.146 +qed
   1.147 +
   1.148 +lemma measure_negligible_finite_Union:
   1.149 +  assumes "finite \<F>"
   1.150 +    and meas: "\<And>S. S \<in> \<F> \<Longrightarrow> S \<in> lmeasurable"
   1.151 +    and djointish: "pairwise (\<lambda>S T. negligible (S \<inter> T)) \<F>"
   1.152 +  shows "measure lebesgue (\<Union>\<F>) = (\<Sum>S\<in>\<F>. measure lebesgue S)"
   1.153 +  using assms
   1.154 +proof (induction)
   1.155 +  case empty
   1.156 +  then show ?case
   1.157 +    by auto
   1.158 +next
   1.159 +  case (insert S \<F>)
   1.160 +  then have "S \<in> lmeasurable" "\<Union>\<F> \<in> lmeasurable" "pairwise (\<lambda>S T. negligible (S \<inter> T)) \<F>"
   1.161 +    by (simp_all add: fmeasurable.finite_Union insert.hyps(1) insert.prems(1) pairwise_insert subsetI)
   1.162 +  then show ?case
   1.163 +  proof (simp add: measure_Un3 insert)
   1.164 +    have *: "\<And>T. T \<in> (\<inter>) S ` \<F> \<Longrightarrow> negligible T"
   1.165 +      using insert by (force simp: pairwise_def)
   1.166 +    have "negligible(S \<inter> \<Union>\<F>)"
   1.167 +      unfolding Int_Union
   1.168 +      by (rule negligible_Union) (simp_all add: * insert.hyps(1))
   1.169 +    then show "measure lebesgue (S \<inter> \<Union>\<F>) = 0"
   1.170 +      using negligible_imp_measure0 by blast
   1.171 +  qed
   1.172 +qed
   1.173 +
   1.174 +lemma measure_negligible_finite_Union_image:
   1.175 +  assumes "finite S"
   1.176 +    and meas: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> lmeasurable"
   1.177 +    and djointish: "pairwise (\<lambda>x y. negligible (f x \<inter> f y)) S"
   1.178 +  shows "measure lebesgue (\<Union>(f ` S)) = (\<Sum>x\<in>S. measure lebesgue (f x))"
   1.179 +proof -
   1.180 +  have "measure lebesgue (\<Union>(f ` S)) = sum (measure lebesgue) (f ` S)"
   1.181 +    using assms by (auto simp: pairwise_mono pairwise_image intro: measure_negligible_finite_Union)
   1.182 +  also have "\<dots> = sum (measure lebesgue \<circ> f) S"
   1.183 +    using djointish [unfolded pairwise_def] by (metis inf.idem negligible_imp_measure0 sum.reindex_nontrivial [OF \<open>finite S\<close>])
   1.184 +  also have "\<dots> = (\<Sum>x\<in>S. measure lebesgue (f x))"
   1.185 +    by simp
   1.186 +  finally show ?thesis .
   1.187 +qed
   1.188 +
   1.189  subsection \<open>Negligibility of a Lipschitz image of a negligible set\<close>
   1.190  
   1.191  text\<open>The bound will be eliminated by a sort of onion argument\<close>
   1.192 @@ -1596,12 +1735,10 @@
   1.193        by (auto simp: fbx_def)
   1.194      have 2: "I' \<subseteq> \<D> \<Longrightarrow> finite I' \<Longrightarrow> measure lebesgue (\<Union>D\<in>I'. fbx D) \<le> e/2" for I'
   1.195        by (rule order_trans[OF measure_Union_le e2]) (auto simp: fbx_def)
   1.196 -    have 3: "0 \<le> e/2"
   1.197 -      using \<open>0<e\<close> by auto
   1.198      show "(\<Union>D\<in>\<D>. fbx D) \<in> lmeasurable"
   1.199 -      by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
   1.200 +      by (intro fmeasurable_UN_bound[OF \<open>countable \<D>\<close> 1 2])
   1.201      have "measure lebesgue (\<Union>D\<in>\<D>. fbx D) \<le> e/2"
   1.202 -      by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2 3])
   1.203 +      by (intro measure_UN_bound[OF \<open>countable \<D>\<close> 1 2])
   1.204      then show "measure lebesgue (\<Union>D\<in>\<D>. fbx D) < e"
   1.205        using \<open>0 < e\<close> by linarith
   1.206    qed
   1.207 @@ -1722,6 +1859,134 @@
   1.208      done
   1.209  qed
   1.210  
   1.211 +subsection\<open>Measurability of countable unions and intersections of various kinds.\<close>
   1.212 +
   1.213 +lemma
   1.214 +  assumes S: "\<And>n. S n \<in> lmeasurable"
   1.215 +    and leB: "\<And>n. measure lebesgue (S n) \<le> B"
   1.216 +    and nest: "\<And>n. S n \<subseteq> S(Suc n)"
   1.217 +  shows measurable_nested_Union: "(\<Union>n. S n) \<in> lmeasurable"
   1.218 +  and measure_nested_Union:  "(\<lambda>n. measure lebesgue (S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. S n)" (is ?Lim)
   1.219 +proof -
   1.220 +  have 1: "\<And>n. (indicat_real (S n)) integrable_on UNIV"
   1.221 +    using S measurable_integrable by blast
   1.222 +  have 2: "\<And>n x::'a. indicat_real (S n) x \<le> (indicat_real (S (Suc n)) x)"
   1.223 +    by (simp add: indicator_leI nest rev_subsetD)
   1.224 +  have 3: "\<And>x. (\<lambda>n. indicat_real (S n) x) \<longlonglongrightarrow> (indicat_real (UNION UNIV S) x)"
   1.225 +    apply (rule Lim_eventually)
   1.226 +    apply (simp add: indicator_def)
   1.227 +    by (metis eventually_sequentiallyI lift_Suc_mono_le nest subsetCE)
   1.228 +  have 4: "bounded (range (\<lambda>n. integral UNIV (indicat_real (S n))))"
   1.229 +    using leB by (auto simp: lmeasure_integral_UNIV [symmetric] S bounded_iff)
   1.230 +  have "(\<Union>n. S n) \<in> lmeasurable \<and> ?Lim"
   1.231 +    apply (simp add: lmeasure_integral_UNIV S cong: conj_cong)
   1.232 +    apply (simp add: measurable_integrable)
   1.233 +    apply (rule monotone_convergence_increasing [OF 1 2 3 4])
   1.234 +    done
   1.235 +  then show "(\<Union>n. S n) \<in> lmeasurable" "?Lim"
   1.236 +    by auto
   1.237 +qed
   1.238 +
   1.239 +lemma
   1.240 +  assumes S: "\<And>n. S n \<in> lmeasurable"
   1.241 +    and djointish: "pairwise (\<lambda>m n. negligible (S m \<inter> S n)) UNIV"
   1.242 +    and leB: "\<And>n. (\<Sum>k\<le>n. measure lebesgue (S k)) \<le> B"
   1.243 +  shows measurable_countable_negligible_Union: "(\<Union>n. S n) \<in> lmeasurable"
   1.244 +  and   measure_countable_negligible_Union:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
   1.245 +proof -
   1.246 +  have 1: "UNION {..n} S \<in> lmeasurable" for n
   1.247 +    using S by blast
   1.248 +  have 2: "measure lebesgue (UNION {..n} S) \<le> B" for n
   1.249 +  proof -
   1.250 +    have "measure lebesgue (UNION {..n} S) \<le> (\<Sum>k\<le>n. measure lebesgue (S k))"
   1.251 +      by (simp add: S fmeasurableD measure_UNION_le)
   1.252 +    with leB show ?thesis
   1.253 +      using order_trans by blast
   1.254 +  qed
   1.255 +  have 3: "\<And>n. UNION {..n} S \<subseteq> UNION {..Suc n} S"
   1.256 +    by (simp add: SUP_subset_mono)
   1.257 +  have eqS: "(\<Union>n. S n) = (\<Union>n. UNION {..n} S)"
   1.258 +    using atLeastAtMost_iff by blast
   1.259 +  also have "(\<Union>n. UNION {..n} S) \<in> lmeasurable"
   1.260 +    by (intro measurable_nested_Union [OF 1 2] 3)
   1.261 +  finally show "(\<Union>n. S n) \<in> lmeasurable" .
   1.262 +  have eqm: "(\<Sum>i\<le>n. measure lebesgue (S i)) = measure lebesgue (UNION {..n} S)" for n
   1.263 +    using assms by (simp add: measure_negligible_finite_Union_image pairwise_mono)
   1.264 +  have "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. UNION {..n} S)"
   1.265 +    by (simp add: sums_def' eqm atLeast0AtMost) (intro measure_nested_Union [OF 1 2] 3)
   1.266 +  then show ?Sums
   1.267 +    by (simp add: eqS)
   1.268 +qed
   1.269 +
   1.270 +lemma negligible_countable_Union [intro]:
   1.271 +  assumes "countable \<F>" and meas: "\<And>S. S \<in> \<F> \<Longrightarrow> negligible S"
   1.272 +  shows "negligible (\<Union>\<F>)"
   1.273 +proof (cases "\<F> = {}")
   1.274 +  case False
   1.275 +  then show ?thesis
   1.276 +    by (metis from_nat_into range_from_nat_into assms negligible_Union_nat)
   1.277 +qed simp
   1.278 +
   1.279 +lemma
   1.280 +  assumes S: "\<And>n. (S n) \<in> lmeasurable"
   1.281 +    and djointish: "pairwise (\<lambda>m n. negligible (S m \<inter> S n)) UNIV"
   1.282 +    and bo: "bounded (\<Union>n. S n)"
   1.283 +  shows measurable_countable_negligible_Union_bounded: "(\<Union>n. S n) \<in> lmeasurable"
   1.284 +  and   measure_countable_negligible_Union_bounded:    "(\<lambda>n. (measure lebesgue (S n))) sums measure lebesgue (\<Union>n. S n)" (is ?Sums)
   1.285 +proof -
   1.286 +  obtain a b where ab: "(\<Union>n. S n) \<subseteq> cbox a b"
   1.287 +    using bo bounded_subset_cbox by blast
   1.288 +  then have B: "(\<Sum>k\<le>n. measure lebesgue (S k)) \<le> measure lebesgue (cbox a b)" for n
   1.289 +  proof -
   1.290 +    have "(\<Sum>k\<le>n. measure lebesgue (S k)) = measure lebesgue (UNION {..n} S)"
   1.291 +      using measure_negligible_finite_Union_image [OF _ _ pairwise_subset] djointish
   1.292 +      by (metis S finite_atMost subset_UNIV)
   1.293 +    also have "\<dots> \<le> measure lebesgue (cbox a b)"
   1.294 +      apply (rule measure_mono_fmeasurable)
   1.295 +      using ab S by force+
   1.296 +    finally show ?thesis .
   1.297 +  qed
   1.298 +  show "(\<Union>n. S n) \<in> lmeasurable"
   1.299 +    by (rule measurable_countable_negligible_Union [OF S djointish B])
   1.300 +  show ?Sums
   1.301 +    by (rule measure_countable_negligible_Union [OF S djointish B])
   1.302 +qed
   1.303 +
   1.304 +lemma measure_countable_Union_approachable:
   1.305 +  assumes "countable \<D>" "e > 0" and measD: "\<And>d. d \<in> \<D> \<Longrightarrow> d \<in> lmeasurable"
   1.306 +      and B: "\<And>D'. \<lbrakk>D' \<subseteq> \<D>; finite D'\<rbrakk> \<Longrightarrow> measure lebesgue (\<Union>D') \<le> B"
   1.307 +    obtains D' where "D' \<subseteq> \<D>" "finite D'" "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (\<Union>D')"
   1.308 +proof (cases "\<D> = {}")
   1.309 +  case True
   1.310 +  then show ?thesis
   1.311 +    by (simp add: \<open>e > 0\<close> that)
   1.312 +next
   1.313 +  case False
   1.314 +  let ?S = "\<lambda>n. \<Union>k \<le> n. from_nat_into \<D> k"
   1.315 +  have "(\<lambda>n. measure lebesgue (?S n)) \<longlonglongrightarrow> measure lebesgue (\<Union>n. ?S n)"
   1.316 +  proof (rule measure_nested_Union)
   1.317 +    show "?S n \<in> lmeasurable" for n
   1.318 +      by (simp add: False fmeasurable.finite_UN from_nat_into measD)
   1.319 +    show "measure lebesgue (?S n) \<le> B" for n
   1.320 +      by (metis (mono_tags, lifting) B False finite_atMost finite_imageI from_nat_into image_iff subsetI)
   1.321 +    show "?S n \<subseteq> ?S (Suc n)" for n
   1.322 +      by force
   1.323 +  qed
   1.324 +  then obtain N where N: "\<And>n. n \<ge> N \<Longrightarrow> dist (measure lebesgue (?S n)) (measure lebesgue (\<Union>n. ?S n)) < e"
   1.325 +    using metric_LIMSEQ_D \<open>e > 0\<close> by blast
   1.326 +  show ?thesis
   1.327 +  proof
   1.328 +    show "from_nat_into \<D> ` {..N} \<subseteq> \<D>"
   1.329 +      by (auto simp: False from_nat_into)
   1.330 +    have eq: "(\<Union>n. \<Union>k\<le>n. from_nat_into \<D> k) = (\<Union>\<D>)"
   1.331 +      using \<open>countable \<D>\<close> False
   1.332 +      by (auto intro: from_nat_into dest: from_nat_into_surj [OF \<open>countable \<D>\<close>])
   1.333 +    show "measure lebesgue (\<Union>\<D>) - e < measure lebesgue (UNION {..N} (from_nat_into \<D>))"
   1.334 +      using N [OF order_refl]
   1.335 +      by (auto simp: eq algebra_simps dist_norm)
   1.336 +  qed auto
   1.337 +qed
   1.338 +
   1.339  subsection\<open>Integral bounds\<close>
   1.340  
   1.341  lemma set_integral_norm_bound:
     2.1 --- a/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Apr 16 05:34:25 2018 +0000
     2.2 +++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Mon Apr 16 15:00:46 2018 +0100
     2.3 @@ -978,8 +978,24 @@
     2.4    and lmeasurable_box [iff]: "box a b \<in> lmeasurable"
     2.5    by (auto simp: fmeasurable_def emeasure_lborel_box_eq emeasure_lborel_cbox_eq)
     2.6  
     2.7 +lemma fmeasurable_compact: "compact S \<Longrightarrow> S \<in> fmeasurable lborel"
     2.8 +  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
     2.9 +
    2.10  lemma lmeasurable_compact: "compact S \<Longrightarrow> S \<in> lmeasurable"
    2.11 -  using emeasure_compact_finite[of S] by (intro fmeasurableI) (auto simp: borel_compact)
    2.12 +  using fmeasurable_compact by (force simp: fmeasurable_def)
    2.13 +
    2.14 +lemma measure_frontier:
    2.15 +   "bounded S \<Longrightarrow> measure lebesgue (frontier S) = measure lebesgue (closure S) - measure lebesgue (interior S)"
    2.16 +  using closure_subset interior_subset
    2.17 +  by (auto simp: frontier_def fmeasurable_compact intro!: measurable_measure_Diff)
    2.18 +
    2.19 +lemma lmeasurable_closure:
    2.20 +   "bounded S \<Longrightarrow> closure S \<in> lmeasurable"
    2.21 +  by (simp add: lmeasurable_compact)
    2.22 +
    2.23 +lemma lmeasurable_frontier:
    2.24 +   "bounded S \<Longrightarrow> frontier S \<in> lmeasurable"
    2.25 +  by (simp add: compact_frontier_bounded lmeasurable_compact)
    2.26  
    2.27  lemma lmeasurable_open: "bounded S \<Longrightarrow> open S \<Longrightarrow> S \<in> lmeasurable"
    2.28    using emeasure_bounded_finite[of S] by (intro fmeasurableI) (auto simp: borel_open)
     3.1 --- a/src/HOL/Analysis/Measure_Space.thy	Mon Apr 16 05:34:25 2018 +0000
     3.2 +++ b/src/HOL/Analysis/Measure_Space.thy	Mon Apr 16 15:00:46 2018 +0100
     3.3 @@ -1749,6 +1749,8 @@
     3.4      using emeasure_mono[of "a - b" a M] * by (auto simp: fmeasurable_def Diff_subset)
     3.5  qed
     3.6  
     3.7 +subsection\<open>Measurable sets formed by unions and intersections\<close>
     3.8 +
     3.9  lemma fmeasurable_Diff: "A \<in> fmeasurable M \<Longrightarrow> B \<in> sets M \<Longrightarrow> A - B \<in> fmeasurable M"
    3.10    using fmeasurableI2[of A M "A - B"] by auto
    3.11  
    3.12 @@ -1882,15 +1884,20 @@
    3.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)"
    3.14    using measure_UNION_le[of F "\<lambda>x. x" M] by simp
    3.15  
    3.16 +text\<open>Version for indexed union over a countable set\<close>
    3.17  lemma
    3.18    assumes "countable I" and I: "\<And>i. i \<in> I \<Longrightarrow> A i \<in> fmeasurable M"
    3.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"
    3.20 +    and bound: "\<And>I'. I' \<subseteq> I \<Longrightarrow> finite I' \<Longrightarrow> measure M (\<Union>i\<in>I'. A i) \<le> B"
    3.21    shows fmeasurable_UN_bound: "(\<Union>i\<in>I. A i) \<in> fmeasurable M" (is ?fm)
    3.22      and measure_UN_bound: "measure M (\<Union>i\<in>I. A i) \<le> B" (is ?m)
    3.23  proof -
    3.24 +  have "B \<ge> 0"
    3.25 +    using bound by force
    3.26    have "?fm \<and> ?m"
    3.27    proof cases
    3.28 -    assume "I = {}" with \<open>0 \<le> B\<close> show ?thesis by simp
    3.29 +    assume "I = {}"
    3.30 +    with \<open>B \<ge> 0\<close> show ?thesis
    3.31 +      by simp
    3.32    next
    3.33      assume "I \<noteq> {}"
    3.34      have "(\<Union>i\<in>I. A i) = (\<Union>i. (\<Union>n\<le>i. A (from_nat_into I n)))"
    3.35 @@ -1918,6 +1925,58 @@
    3.36    then show ?fm ?m by auto
    3.37  qed
    3.38  
    3.39 +text\<open>Version for big union of a countable set\<close>
    3.40 +lemma
    3.41 +  assumes "countable \<D>"
    3.42 +    and meas: "\<And>D. D \<in> \<D> \<Longrightarrow> D \<in> fmeasurable M"
    3.43 +    and bound:  "\<And>\<E>. \<lbrakk>\<E> \<subseteq> \<D>; finite \<E>\<rbrakk> \<Longrightarrow> measure M (\<Union>\<E>) \<le> B"
    3.44 + shows fmeasurable_Union_bound: "\<Union>\<D> \<in> fmeasurable M"  (is ?fm)
    3.45 +    and measure_Union_bound: "measure M (\<Union>\<D>) \<le> B"     (is ?m)
    3.46 +proof -
    3.47 +  have "B \<ge> 0"
    3.48 +    using bound by force
    3.49 +  have "?fm \<and> ?m"
    3.50 +  proof (cases "\<D> = {}")
    3.51 +    case True
    3.52 +    with \<open>B \<ge> 0\<close> show ?thesis
    3.53 +      by auto
    3.54 +  next
    3.55 +    case False
    3.56 +    then obtain D :: "nat \<Rightarrow> 'a set" where D: "\<D> = range D"
    3.57 +      using \<open>countable \<D>\<close> uncountable_def by force
    3.58 +      have 1: "\<And>i. D i \<in> fmeasurable M"
    3.59 +        by (simp add: D meas)
    3.60 +      have 2: "\<And>I'. finite I' \<Longrightarrow> measure M (\<Union>x\<in>I'. D x) \<le> B"
    3.61 +        by (simp add: D bound image_subset_iff)
    3.62 +      show ?thesis
    3.63 +        unfolding D
    3.64 +        by (intro conjI fmeasurable_UN_bound [OF _ 1 2] measure_UN_bound [OF _ 1 2]) auto
    3.65 +    qed
    3.66 +    then show ?fm ?m by auto
    3.67 +qed
    3.68 +
    3.69 +text\<open>Version for indexed union over the type of naturals\<close>
    3.70 +lemma
    3.71 +  fixes S :: "nat \<Rightarrow> 'a set"
    3.72 +  assumes S: "\<And>i. S i \<in> fmeasurable M" and B: "\<And>n. measure M (\<Union>i\<le>n. S i) \<le> B"
    3.73 +  shows fmeasurable_countable_Union: "(\<Union>i. S i) \<in> fmeasurable M"
    3.74 +    and measure_countable_Union_le: "measure M (\<Union>i. S i) \<le> B"
    3.75 +proof -
    3.76 +  have mB: "measure M (\<Union>i\<in>I. S i) \<le> B" if "finite I" for I
    3.77 +  proof -
    3.78 +    have "(\<Union>i\<in>I. S i) \<subseteq> (\<Union>i\<le>Max I. S i)"
    3.79 +      using Max_ge that by force
    3.80 +    then have "measure M (\<Union>i\<in>I. S i) \<le> measure M (\<Union>i \<le> Max I. S i)"
    3.81 +      by (rule measure_mono_fmeasurable) (use S in \<open>blast+\<close>)
    3.82 +    then show ?thesis
    3.83 +      using B order_trans by blast
    3.84 +  qed
    3.85 +  show "(\<Union>i. S i) \<in> fmeasurable M"
    3.86 +    by (auto intro: fmeasurable_UN_bound [OF _ S mB])
    3.87 +  show "measure M (\<Union>n. S n) \<le> B"
    3.88 +    by (auto intro: measure_UN_bound [OF _ S mB])
    3.89 +qed
    3.90 +
    3.91  lemma measure_diff_le_measure_setdiff:
    3.92    assumes "S \<in> fmeasurable M" "T \<in> fmeasurable M"
    3.93    shows "measure M S - measure M T \<le> measure M (S - T)"
     4.1 --- a/src/HOL/Analysis/Starlike.thy	Mon Apr 16 05:34:25 2018 +0000
     4.2 +++ b/src/HOL/Analysis/Starlike.thy	Mon Apr 16 15:00:46 2018 +0100
     4.3 @@ -8421,6 +8421,83 @@
     4.4    apply (simp add: adjoint_works assms(1) inner_commute)
     4.5    by (metis adjoint_works all_zero_iff assms(1) inner_commute)
     4.6  
     4.7 +subsection\<open> A non-injective linear function maps into a hyperplane.\<close>
     4.8 +
     4.9 +lemma linear_surj_adj_imp_inj:
    4.10 +  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
    4.11 +  assumes "linear f" "surj (adjoint f)"
    4.12 +  shows "inj f"
    4.13 +proof -
    4.14 +  have "\<exists>x. y = adjoint f x" for y
    4.15 +    using assms by (simp add: surjD)
    4.16 +  then show "inj f"
    4.17 +    using assms unfolding inj_on_def image_def
    4.18 +    by (metis (no_types) adjoint_works euclidean_eqI)
    4.19 +qed
    4.20 +
    4.21 +(*http://mathonline.wikidot.com/injectivity-and-surjectivity-of-the-adjoint-of-a-linear-map*)
    4.22 +lemma surj_adjoint_iff_inj [simp]:
    4.23 +  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
    4.24 +  assumes "linear f"
    4.25 +  shows  "surj (adjoint f) \<longleftrightarrow> inj f"
    4.26 +proof
    4.27 +  assume "surj (adjoint f)"
    4.28 +  then show "inj f"
    4.29 +    by (simp add: assms linear_surj_adj_imp_inj)
    4.30 +next
    4.31 +  assume "inj f"
    4.32 +  have "f -` {0} = {0}"
    4.33 +    using assms \<open>inj f\<close> linear_0 linear_injective_0 by fastforce
    4.34 +  moreover have "f -` {0} = range (adjoint f)\<^sup>\<bottom>"
    4.35 +    by (intro ker_orthogonal_comp_adjoint assms)
    4.36 +  ultimately have "range (adjoint f)\<^sup>\<bottom>\<^sup>\<bottom> = UNIV"
    4.37 +    by (metis orthogonal_comp_null)
    4.38 +  then show "surj (adjoint f)"
    4.39 +    by (simp add: adjoint_linear \<open>linear f\<close> subspace_linear_image orthogonal_comp_self)
    4.40 +qed
    4.41 +
    4.42 +lemma inj_adjoint_iff_surj [simp]:
    4.43 +  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
    4.44 +  assumes "linear f"
    4.45 +  shows  "inj (adjoint f) \<longleftrightarrow> surj f"
    4.46 +proof
    4.47 +  assume "inj (adjoint f)"
    4.48 +  have "(adjoint f) -` {0} = {0}"
    4.49 +    by (metis \<open>inj (adjoint f)\<close> adjoint_linear assms surj_adjoint_iff_inj ker_orthogonal_comp_adjoint orthogonal_comp_UNIV)
    4.50 +  then have "(range(f))\<^sup>\<bottom> = {0}"
    4.51 +    by (metis (no_types, hide_lams) adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint set_zero)
    4.52 +  then show "surj f"
    4.53 +    by (metis \<open>inj (adjoint f)\<close> adjoint_adjoint adjoint_linear assms surj_adjoint_iff_inj)
    4.54 +next
    4.55 +  assume "surj f"
    4.56 +  then have "range f = (adjoint f -` {0})\<^sup>\<bottom>"
    4.57 +    by (simp add: adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint)
    4.58 +  then have "{0} = adjoint f -` {0}"
    4.59 +    using \<open>surj f\<close> adjoint_adjoint adjoint_linear assms ker_orthogonal_comp_adjoint by force
    4.60 +  then show "inj (adjoint f)"
    4.61 +    by (simp add: \<open>surj f\<close> adjoint_adjoint adjoint_linear assms linear_surj_adj_imp_inj)
    4.62 +qed
    4.63 +
    4.64 +proposition linear_singular_into_hyperplane:
    4.65 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
    4.66 +  assumes "linear f"
    4.67 +  shows "\<not> inj f \<longleftrightarrow> (\<exists>a. a \<noteq> 0 \<and> (\<forall>x. a \<bullet> f x = 0))" (is "_ = ?rhs")
    4.68 +proof
    4.69 +  assume "\<not>inj f"
    4.70 +  then show ?rhs
    4.71 +    using all_zero_iff
    4.72 +    by (metis (no_types, hide_lams) adjoint_clauses(2) adjoint_linear assms linear_injective_0 linear_injective_imp_surjective linear_surj_adj_imp_inj)
    4.73 +next
    4.74 +  assume ?rhs
    4.75 +  then show "\<not>inj f"
    4.76 +    by (metis assms linear_injective_isomorphism all_zero_iff)
    4.77 +qed
    4.78 +
    4.79 +lemma linear_singular_image_hyperplane:
    4.80 +  fixes f :: "'n::euclidean_space \<Rightarrow> 'n"
    4.81 +  assumes "linear f" "\<not>inj f"
    4.82 +  obtains a where "a \<noteq> 0" "\<And>S. f ` S \<subseteq> {x. a \<bullet> x = 0}"
    4.83 +  using assms by (fastforce simp add: linear_singular_into_hyperplane)
    4.84  
    4.85  end
    4.86