# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1523797020 -3600
# Node ID 7643b005b29abc26fac98dbfc741804fdf18e95f
# Parent  349c639e593cd24d1d3b3c17c8808a1fc18708b4
various new results on measures, integrals, etc., and some simplified proofs

diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Ball_Volume.thy
--- a/src/HOL/Analysis/Ball_Volume.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Ball_Volume.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -1,10 +1,10 @@
 (*  
    File:     HOL/Analysis/Gamma_Function.thy
    Author:   Manuel Eberl, TU München
+*)
 
-   The volume (Lebesgue measure) of an n-dimensional ball.
-*)
-section \<open>The volume of an $n$-ball\<close>
+section \<open>The volume (Lebesgue measure) of an $n$-dimensional ball\<close>
+
 theory Ball_Volume
   imports Gamma_Function Lebesgue_Integral_Substitution
 begin
@@ -301,4 +301,30 @@
 corollary sphere_volume: "r \<ge> 0 \<Longrightarrow> content (ball c r :: (real ^ 3) set) = 4 / 3 * r ^ 3 * pi"
   by (simp add: content_ball unit_ball_vol_3)
 
+text \<open>
+  Useful equivalent forms
+\<close>
+corollary content_ball_eq_0_iff [simp]: "content (ball c r) = 0 \<longleftrightarrow> r \<le> 0"
+proof -
+  have "r > 0 \<Longrightarrow> content (ball c r) > 0"
+    by (simp add: content_ball unit_ball_vol_def)
+  then show ?thesis
+    by (fastforce simp: ball_empty)
+qed
+
+corollary content_ball_gt_0_iff [simp]: "0 < content (ball z r) \<longleftrightarrow> 0 < r"
+  by (auto simp: zero_less_measure_iff)
+
+corollary content_cball_eq_0_iff [simp]: "content (cball c r) = 0 \<longleftrightarrow> r \<le> 0"
+proof (cases "r = 0")
+  case False
+  moreover have "r > 0 \<Longrightarrow> content (cball c r) > 0"
+    by (simp add: content_cball unit_ball_vol_def)
+  ultimately show ?thesis
+    by fastforce
+qed auto
+
+corollary content_cball_gt_0_iff [simp]: "0 < content (cball z r) \<longleftrightarrow> 0 < r"
+  by (auto simp: zero_less_measure_iff)
+
 end
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -4,6 +4,16 @@
 imports Finite_Cartesian_Product Derivative
 begin
 
+lemma norm_le_componentwise:
+   "(\<And>b. b \<in> Basis \<Longrightarrow> abs(x \<bullet> b) \<le> abs(y \<bullet> b)) \<Longrightarrow> norm x \<le> norm y"
+  by (auto simp: norm_le euclidean_inner [of x x] euclidean_inner [of y y] abs_le_square_iff power2_eq_square intro!: sum_mono)
+
+lemma norm_le_componentwise_cart:
+  fixes x :: "real^'n"
+  shows "(\<And>i. abs(x$i) \<le> abs(y$i)) \<Longrightarrow> norm x \<le> norm y"
+  unfolding cart_eq_inner_axis
+  by (rule norm_le_componentwise) (metis axis_index)
+  
 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
   by (simp add: subspace_def)
 
@@ -759,7 +769,7 @@
   have "norm (\<chi> j. A $ j $ i) \<le> norm (A *v axis i 1)"
     by (simp add: matrix_mult_dot cart_eq_inner_axis)
   also have "\<dots> \<le> onorm (( *v) A)"
-    using onorm [OF bl, of "axis i 1"] by (auto simp: axis_in_Basis)
+    using onorm [OF bl, of "axis i 1"] by auto
   finally have "norm (\<chi> j. A $ j $ i) \<le> onorm (( *v) A)" .
   then show ?thesis
     unfolding column_def .
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Complete_Measure.thy
--- a/src/HOL/Analysis/Complete_Measure.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Complete_Measure.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -114,6 +114,11 @@
   qed auto
 qed
 
+lemma sets_restrict_space_subset:
+  assumes S: "S \<in> sets (completion M)"
+  shows "sets (restrict_space (completion M) S) \<subseteq> sets (completion M)"
+  by (metis assms sets.Int_space_eq2 sets_restrict_space_iff subsetI)
+
 lemma
   assumes "S \<in> sets (completion M)"
   shows main_part_sets[intro, simp]: "main_part M S \<in> sets M"
@@ -989,6 +994,23 @@
   finally show ?thesis .
 qed
 
+lemma (in complete_measure) fmeasurable_measure_inner_outer_le:
+     "(S \<in> fmeasurable M \<and> m = measure M S) \<longleftrightarrow>
+        (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e \<le> measure M T) \<and>
+        (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U \<le> m + e)" (is ?T1)
+  and null_sets_outer_le:
+     "S \<in> null_sets M \<longleftrightarrow> (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T \<le> e)" (is ?T2)
+proof -
+  have "e > 0 \<and> m - e/2 \<le> t \<Longrightarrow> m - e < t"
+       "e > 0 \<and> t \<le> m + e/2 \<Longrightarrow> t < m + e"
+       "e > 0 \<longleftrightarrow> e/2 > 0"
+       for e t
+    by auto
+  then show ?T1 ?T2
+    unfolding fmeasurable_measure_inner_outer null_sets_outer
+    by (meson dense le_less_trans less_imp_le)+
+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>
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -6992,7 +6992,7 @@
     done
 qed
 
-subsubsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
+subsection%unimportant\<open>Representation of any interval as a finite convex hull\<close>
 
 lemma image_stretch_interval:
   "(\<lambda>x. \<Sum>k\<in>Basis. (m k * (x\<bullet>k)) *\<^sub>R k) ` cbox a (b::'a::euclidean_space) =
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -945,7 +945,18 @@
       by (auto simp: integrable_on_def nn_integral_completion)
   qed
 qed
-  
+
+lemma integrable_on_lebesgue_on:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "integrable (lebesgue_on S) f" and S: "S \<in> sets lebesgue"
+  shows "f integrable_on S"
+proof -
+  have "integrable lebesgue (\<lambda>x. indicator S x *\<^sub>R f x)"
+    using S f inf_top.comm_neutral integrable_restrict_space by blast
+  then show ?thesis
+    using absolutely_integrable_on_def set_integrable_def by blast
+qed
+
 lemma absolutely_integrable_on_null [intro]:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "content (cbox a b) = 0 \<Longrightarrow> f absolutely_integrable_on (cbox a b)"
@@ -1051,6 +1062,39 @@
 lemma lmeasure_integral: "S \<in> lmeasurable \<Longrightarrow> measure lebesgue S = integral S (\<lambda>x. 1::real)"
   by (fastforce simp add: lmeasure_integral_UNIV indicator_def[abs_def] lmeasurable_iff_integrable_on)
 
+lemma integrable_on_const: "S \<in> lmeasurable \<Longrightarrow> (\<lambda>x. c) integrable_on S"
+  unfolding lmeasurable_iff_integrable
+  by (metis (mono_tags, lifting) integrable_eq integrable_on_scaleR_left lmeasurable_iff_integrable lmeasurable_iff_integrable_on scaleR_one)
+
+lemma integral_indicator:
+  assumes "(S \<inter> T) \<in> lmeasurable"
+  shows "integral T (indicator S) = measure lebesgue (S \<inter> T)"
+proof -
+  have "integral UNIV (indicator (S \<inter> T)) = integral UNIV (\<lambda>a. if a \<in> S \<inter> T then 1::real else 0)"
+    by (meson indicator_def)
+  moreover
+  have "(indicator (S \<inter> T) has_integral measure lebesgue (S \<inter> T)) UNIV"
+    using assms by (simp add: lmeasurable_iff_has_integral)
+  ultimately have "integral UNIV (\<lambda>x. if x \<in> S \<inter> T then 1 else 0) = measure lebesgue (S \<inter> T)"
+    by (metis (no_types) integral_unique)
+  then show ?thesis
+    using integral_restrict_Int [of UNIV "S \<inter> T" "\<lambda>x. 1::real"]
+    apply (simp add: integral_restrict_Int [symmetric])
+    by (meson indicator_def)
+qed
+
+lemma measurable_integrable:
+  fixes S :: "'a::euclidean_space set"
+  shows "S \<in> lmeasurable \<longleftrightarrow> (indicat_real S) integrable_on UNIV"
+  by (auto simp: lmeasurable_iff_integrable absolutely_integrable_on_iff_nonneg [symmetric] set_integrable_def)
+
+lemma integrable_on_indicator:
+  fixes S :: "'a::euclidean_space set"
+  shows "indicat_real S integrable_on T \<longleftrightarrow> (S \<inter> T) \<in> lmeasurable"
+  unfolding measurable_integrable
+  unfolding integrable_restrict_UNIV [of T, symmetric]
+  by (fastforce simp add: indicator_def elim: integrable_eq)
+
 lemma
   assumes \<D>: "\<D> division_of S"
   shows lmeasurable_division: "S \<in> lmeasurable" (is ?l)
@@ -1072,7 +1116,6 @@
     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
   assume "negligible S"
@@ -2208,6 +2251,12 @@
     using f by (auto intro: has_integral_implies_lebesgue_measurable simp: integrable_on_def)
 qed (use le in \<open>force intro!: always_eventually split: split_indicator\<close>)
 
+lemma absolutely_integrable_continuous:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "continuous_on (cbox a b) f \<Longrightarrow> f absolutely_integrable_on cbox a b"
+  using absolutely_integrable_integrable_bound
+  by (simp add: absolutely_integrable_on_def continuous_on_norm integrable_continuous)
+
 subsection \<open>Componentwise\<close>
 
 proposition absolutely_integrable_componentwise_iff:
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Fashoda_Theorem.thy
--- a/src/HOL/Analysis/Fashoda_Theorem.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Fashoda_Theorem.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -269,15 +269,10 @@
       by auto
     moreover
     from x1 have "g (x $ 2) \<in> cbox (-1) 1"
-      apply -
-      apply (rule assms(2)[unfolded subset_eq,rule_format])
-      apply auto
-      done
+      using assms(2) by blast
     ultimately show False
       unfolding lem3[OF nz] vector_component_simps * mem_box_cart
-      apply (erule_tac x=1 in allE)
-      apply auto
-      done
+      using not_le by auto
   next
     assume as: "x$1 = -1"
     then have *: "f (x $ 1) $ 1 = - 1"
@@ -288,15 +283,10 @@
       by auto
     moreover
     from x1 have "g (x $ 2) \<in> cbox (-1) 1"
-      apply -
-      apply (rule assms(2)[unfolded subset_eq,rule_format])
-      apply auto
-      done
+      using assms(2) by blast
     ultimately show False
       unfolding lem3[OF nz] vector_component_simps * mem_box_cart
-      apply (erule_tac x=1 in allE)
-      apply auto
-      done
+      using not_le by auto
   next
     assume as: "x$2 = 1"
     then have *: "g (x $ 2) $ 2 = 1"
@@ -527,7 +517,7 @@
       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1"
       and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1"
       using assms as
-      by (simp_all add: axis_in_Basis cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
+      by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def)
          (simp_all add: inner_axis)
   qed
   from z(1) obtain zf where zf:
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -607,20 +607,8 @@
   apply (rule sum.neutral, simp add: axis_def)
   done
 
-lemma sum_single:
-  assumes "finite A" and "k \<in> A" and "f k = y"
-  assumes "\<And>i. i \<in> A \<Longrightarrow> i \<noteq> k \<Longrightarrow> f i = 0"
-  shows "(\<Sum>i\<in>A. f i) = y"
-  apply (subst sum.remove [OF assms(1,2)])
-  apply (simp add: sum.neutral assms(3,4))
-  done
-
 lemma inner_axis: "inner x (axis i y) = inner (x $ i) y"
-  unfolding inner_vec_def
-  apply (rule_tac k=i in sum_single)
-  apply simp_all
-  apply (simp add: axis_def)
-  done
+  by (simp add: inner_vec_def axis_def sum.remove [where x=i])
 
 lemma inner_axis': "inner(axis i y) x = inner y (x $ i)"
   by (simp add: inner_axis inner_commute)
@@ -649,22 +637,51 @@
     by (simp add: inner_axis euclidean_all_zero_iff vec_eq_iff)
 qed
 
-lemma DIM_cart[simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
-  apply (simp add: Basis_vec_def)
-  apply (subst card_UN_disjoint)
-     apply simp
-    apply simp
-   apply (auto simp: axis_eq_axis) [1]
-  apply (subst card_UN_disjoint)
-     apply (auto simp: axis_eq_axis)
-  done
+lemma DIM_cart [simp]: "DIM('a^'b) = CARD('b) * DIM('a)"
+proof -
+  have "card (\<Union>i::'b. \<Union>u::'a\<in>Basis. {axis i u}) = (\<Sum>i::'b\<in>UNIV. card (\<Union>u::'a\<in>Basis. {axis i u}))"
+    by (rule card_UN_disjoint) (auto simp: axis_eq_axis) 
+  also have "... = CARD('b) * DIM('a)"
+    by (subst card_UN_disjoint) (auto simp: axis_eq_axis)
+  finally show ?thesis
+    by (simp add: Basis_vec_def)
+qed
 
 end
 
 lemma cart_eq_inner_axis: "a $ i = inner a (axis i 1)"
   by (simp add: inner_axis)
 
-lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis"
-  by (auto simp add: Basis_vec_def axis_eq_axis)
+lemma axis_eq_0_iff [simp]:
+  shows "axis m x = 0 \<longleftrightarrow> x = 0"
+  by (simp add: axis_def vec_eq_iff)
+
+lemma axis_in_Basis_iff [simp]: "axis i a \<in> Basis \<longleftrightarrow> a \<in> Basis"
+  by (auto simp: Basis_vec_def axis_eq_axis)
+
+text\<open>Mapping each basis element to the corresponding finite index\<close>
+definition axis_index :: "('a::comm_ring_1)^'n \<Rightarrow> 'n" where "axis_index v \<equiv> SOME i. v = axis i 1"
+
+lemma axis_inverse:
+  fixes v :: "real^'n"
+  assumes "v \<in> Basis"
+  shows "\<exists>i. v = axis i 1"
+proof -
+  have "v \<in> (\<Union>n. \<Union>r\<in>Basis. {axis n r})"
+    using assms Basis_vec_def by blast
+  then show ?thesis
+    by (force simp add: vec_eq_iff)
+qed
+
+lemma axis_index:
+  fixes v :: "real^'n"
+  assumes "v \<in> Basis"
+  shows "v = axis (axis_index v) 1"
+  by (metis (mono_tags) assms axis_inverse axis_index_def someI_ex)
+
+lemma axis_index_axis [simp]:
+  fixes UU :: "real^'n"
+  shows "(axis_index (axis u 1 :: real^'n)) = (u::'n)"
+  by (simp add: axis_eq_axis axis_index_def)
 
 end
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -3501,6 +3501,44 @@
   using assms unfolding integrable_on_def
   by (force dest: has_integral_stretch)
 
+lemma vec_lambda_eq_sum:
+  shows "(\<chi> k. f k (x $ k)) = (\<Sum>k\<in>Basis. (f (axis_index k) (x \<bullet> k)) *\<^sub>R k)"
+    apply (simp add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
+    apply (simp add: vec_eq_iff axis_def if_distrib cong: if_cong)
+    done
+
+lemma has_integral_stretch_cart:
+  fixes m :: "'n::finite \<Rightarrow> real"
+  assumes f: "(f has_integral i) (cbox a b)" and m: "\<And>k. m k \<noteq> 0"
+  shows "((\<lambda>x. f(\<chi> k. m k * x$k)) has_integral i /\<^sub>R \<bar>prod m UNIV\<bar>)
+            ((\<lambda>x. \<chi> k. x$k / m k) ` (cbox a b))"
+proof -
+  have *: "\<forall>k:: real^'n \<in> Basis. m (axis_index k) \<noteq> 0"
+    using axis_index by (simp add: m)
+  have eqp: "(\<Prod>k:: real^'n \<in> Basis. m (axis_index k)) = prod m UNIV"
+    by (simp add: Basis_vec_def UNION_singleton_eq_range prod.reindex axis_eq_axis inj_on_def)
+  show ?thesis
+    using has_integral_stretch [OF f *] vec_lambda_eq_sum [where f="\<lambda>i x. m i * x"] vec_lambda_eq_sum [where f="\<lambda>i x. x / m i"]
+    by (simp add: field_simps eqp)
+qed
+
+lemma image_stretch_interval_cart:
+  fixes m :: "'n::finite \<Rightarrow> real"
+  shows "(\<lambda>x. \<chi> k. m k * x$k) ` cbox a b =
+            (if cbox a b = {} then {}
+            else cbox (\<chi> k. min (m k * a$k) (m k * b$k)) (\<chi> k. max (m k * a$k) (m k * b$k)))"
+proof -
+  have *: "(\<Sum>k\<in>Basis. min (m (axis_index k) * (a \<bullet> k)) (m (axis_index k) * (b \<bullet> k)) *\<^sub>R k)
+           = (\<chi> k. min (m k * a $ k) (m k * b $ k))"
+          "(\<Sum>k\<in>Basis. max (m (axis_index k) * (a \<bullet> k)) (m (axis_index k) * (b \<bullet> k)) *\<^sub>R k)
+           = (\<chi> k. max (m k * a $ k) (m k * b $ k))"
+    apply (simp_all add: Basis_vec_def cart_eq_inner_axis UNION_singleton_eq_range sum.reindex axis_eq_axis inj_on_def)
+    apply (simp_all add: vec_eq_iff axis_def if_distrib cong: if_cong)
+    done
+  show ?thesis
+    by (simp add: vec_lambda_eq_sum [where f="\<lambda>i x. m i * x"] image_stretch_interval eq_cbox *)
+qed
+
 
 subsection \<open>even more special cases\<close>
 
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -393,6 +393,23 @@
 lemma Compl_in_sets_lebesgue: "-A \<in> sets lebesgue \<longleftrightarrow> A  \<in> sets lebesgue"
   by (metis Compl_eq_Diff_UNIV double_compl space_borel space_completion space_lborel Sigma_Algebra.sets.compl_sets)
 
+lemma measurable_lebesgue_cong:
+  assumes "\<And>x. x \<in> S \<Longrightarrow> f x = g x"
+  shows "f \<in> measurable (lebesgue_on S) M \<longleftrightarrow> g \<in> measurable (lebesgue_on S) M"
+  by (metis (mono_tags, lifting) IntD1 assms measurable_cong_strong space_restrict_space)
+
+text\<open>Measurability of continuous functions\<close>
+lemma continuous_imp_measurable_on_sets_lebesgue:
+  assumes f: "continuous_on S f" and S: "S \<in> sets lebesgue"
+  shows "f \<in> borel_measurable (lebesgue_on S)"
+proof -
+  have "sets (restrict_space borel S) \<subseteq> sets (lebesgue_on S)"
+    by (simp add: mono_restrict_space subsetI)
+  then show ?thesis
+    by (simp add: borel_measurable_continuous_on_restrict [OF f] borel_measurable_subalgebra 
+                  space_restrict_space)
+qed
+
 context
 begin
 
@@ -446,7 +463,7 @@
 
 lemma AE_lborel_singleton: "AE x in lborel::'a::euclidean_space measure. x \<noteq> c"
   using SOME_Basis AE_discrete_difference [of "{c}" lborel] emeasure_lborel_cbox [of c c]
-  by (auto simp add: cbox_sing prod_constant power_0_left)
+  by (auto simp add: power_0_left)
 
 lemma emeasure_lborel_Ioo[simp]:
   assumes [simp]: "l \<le> u"
@@ -542,7 +559,7 @@
 
 end
 
-lemma emeasure_lborel_UNIV: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
+lemma emeasure_lborel_UNIV [simp]: "emeasure lborel (UNIV::'a::euclidean_space set) = \<infinity>"
 proof -
   { fix n::nat
     let ?Ba = "Basis :: 'a set"
@@ -949,6 +966,9 @@
 where
   "lmeasurable \<equiv> fmeasurable lebesgue"
 
+lemma not_measurable_UNIV [simp]: "UNIV \<notin> lmeasurable"
+  by (simp add: fmeasurable_def)
+
 lemma lmeasurable_iff_integrable:
   "S \<in> lmeasurable \<longleftrightarrow> integrable lebesgue (indicator S :: 'a::euclidean_space \<Rightarrow> real)"
   by (auto simp: fmeasurable_def integrable_iff_bounded borel_measurable_indicator_iff ennreal_indicator)
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -1962,15 +1962,43 @@
 lemma linear_bounded_pos:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes lf: "linear f"
-  shows "\<exists>B > 0. \<forall>x. norm (f x) \<le> B * norm x"
+ obtains B where "B > 0" "\<And>x. norm (f x) \<le> B * norm x"
 proof -
   have "\<exists>B > 0. \<forall>x. norm (f x) \<le> norm x * B"
     using lf unfolding linear_conv_bounded_linear
     by (rule bounded_linear.pos_bounded)
-  then show ?thesis
-    by (simp only: mult.commute)
+  with that show ?thesis
+    by (auto simp: mult.commute)
 qed
 
+lemma linear_invertible_bounded_below_pos:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "linear g" "g \<circ> f = id"
+  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
+proof -
+  obtain B where "B > 0" and B: "\<And>x. norm (g x) \<le> B * norm x"
+    using linear_bounded_pos [OF \<open>linear g\<close>] by blast
+  show thesis
+  proof
+    show "0 < 1/B"
+      by (simp add: \<open>B > 0\<close>)
+    show "1/B * norm x \<le> norm (f x)" for x
+    proof -
+      have "1/B * norm x = 1/B * norm (g (f x))"
+        using assms by (simp add: pointfree_idE)
+      also have "\<dots> \<le> norm (f x)"
+        using B [of "f x"] by (simp add: \<open>B > 0\<close> mult.commute pos_divide_le_eq)
+      finally show ?thesis .
+    qed
+  qed
+qed
+
+lemma linear_inj_bounded_below_pos:
+  fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::euclidean_space"
+  assumes "linear f" "inj f"
+  obtains B where "B > 0" "\<And>x. B * norm x \<le> norm(f x)"
+  using linear_injective_left_inverse [OF assms] linear_invertible_bounded_below_pos assms by blast
+
 lemma bounded_linearI':
   fixes f ::"'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
   assumes "\<And>x y. f (x + y) = f x + f y"
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Measure_Space.thy
--- a/src/HOL/Analysis/Measure_Space.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Measure_Space.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -1534,6 +1534,9 @@
 lemma measure_nonneg[simp]: "0 \<le> measure M A"
   unfolding measure_def by auto
 
+lemma measure_nonneg' [simp]: "\<not> measure M A < 0"
+  using measure_nonneg not_le by blast
+
 lemma zero_less_measure_iff: "0 < measure M A \<longleftrightarrow> measure M A \<noteq> 0"
   using measure_nonneg[of M A] by (auto simp add: le_less)
 
@@ -1686,7 +1689,7 @@
   moreover have "ennreal (measure M (A i)) = emeasure M (A i)" for i
     using assms emeasure_mono[of "A _" "\<Union>i. A i" M]
     by (intro emeasure_eq_ennreal_measure[symmetric]) (auto simp: less_top UN_upper intro: le_less_trans)
-  ultimately show "(\<lambda>x. ennreal (Sigma_Algebra.measure M (A x))) \<longlonglongrightarrow> ennreal (Sigma_Algebra.measure M (\<Union>i. A i))"
+  ultimately show "(\<lambda>x. ennreal (measure M (A x))) \<longlonglongrightarrow> ennreal (measure M (\<Union>i. A i))"
     using A by (auto intro!: Lim_emeasure_incseq)
 qed auto
 
@@ -1699,7 +1702,7 @@
     by (auto intro!: emeasure_eq_ennreal_measure[symmetric] simp: INT_lower less_top intro: le_less_trans)
   moreover have "ennreal (measure M (A i)) = emeasure M (A i)" for i
     using A fin[of i] by (intro emeasure_eq_ennreal_measure[symmetric]) auto
-  ultimately show "(\<lambda>x. ennreal (Sigma_Algebra.measure M (A x))) \<longlonglongrightarrow> ennreal (Sigma_Algebra.measure M (\<Inter>i. A i))"
+  ultimately show "(\<lambda>x. ennreal (measure M (A x))) \<longlonglongrightarrow> ennreal (measure M (\<Inter>i. A i))"
     using fin A by (auto intro!: Lim_emeasure_decseq)
 qed auto
 
@@ -1772,6 +1775,32 @@
     using assms by (intro sets.countable_INT') auto
 qed
 
+lemma measurable_measure_Diff:
+  assumes "A \<in> fmeasurable M" "B \<in> sets M" "B \<subseteq> A"
+  shows "measure M (A - B) = measure M A - measure M B"
+  by (simp add: assms fmeasurableD fmeasurableD2 measure_Diff)
+
+lemma measurable_Un_null_set:
+  assumes "B \<in> null_sets M"
+  shows "(A \<union> B \<in> fmeasurable M \<and> A \<in> sets M) \<longleftrightarrow> A \<in> fmeasurable M"
+  using assms  by (fastforce simp add: fmeasurable.Un fmeasurableI_null_sets intro: fmeasurableI2)
+
+lemma measurable_Diff_null_set:
+  assumes "B \<in> null_sets M"
+  shows "(A - B) \<in> fmeasurable M \<and> A \<in> sets M \<longleftrightarrow> A \<in> fmeasurable M"
+  using assms
+  by (metis Un_Diff_cancel2 fmeasurable.Diff fmeasurableD fmeasurableI_null_sets measurable_Un_null_set)
+
+lemma fmeasurable_Diff_D:
+    assumes m: "T - S \<in> fmeasurable M" "S \<in> fmeasurable M" and sub: "S \<subseteq> T"
+    shows "T \<in> fmeasurable M"
+proof -
+  have "T = S \<union> (T - S)"
+    using assms by blast
+  then show ?thesis
+    by (metis m fmeasurable.Un)
+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)
@@ -1801,12 +1830,13 @@
     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
+proof (induction I rule: finite_induct)
+  case (insert x I)
+  have "measure M (F x \<union> UNION I F) = measure M (F x) + measure M (UNION I F)"
+    by (rule measure_Un_AE) (use insert in \<open>auto simp: pairwise_insert\<close>)
+    with insert show ?case
+      by (simp add: pairwise_insert )
+qed simp
 
 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>
@@ -1888,6 +1918,18 @@
   then show ?fm ?m by auto
 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)"
+proof -
+  have "measure M S \<le> measure M ((S - T) \<union> T)"
+    by (simp add: assms fmeasurable.Un fmeasurableD measure_mono_fmeasurable)
+  also have "\<dots> \<le> measure M (S - T) + measure M T"
+    using assms by (blast intro: measure_Un_le)
+  finally show ?thesis
+    by (simp add: algebra_simps)
+qed
+
 lemma suminf_exist_split2:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   assumes "summable f"
diff -r 349c639e593c -r 7643b005b29a src/HOL/Analysis/Sigma_Algebra.thy
--- a/src/HOL/Analysis/Sigma_Algebra.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Analysis/Sigma_Algebra.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -2096,7 +2096,7 @@
 lemma space_restrict_space: "space (restrict_space M \<Omega>) = \<Omega> \<inter> space M"
   using sets.sets_into_space unfolding restrict_space_def by (subst space_measure_of) auto
 
-lemma space_restrict_space2: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
+lemma space_restrict_space2 [simp]: "\<Omega> \<in> sets M \<Longrightarrow> space (restrict_space M \<Omega>) = \<Omega>"
   by (simp add: space_restrict_space sets.sets_into_space)
 
 lemma sets_restrict_space: "sets (restrict_space M \<Omega>) = ((\<inter>) \<Omega>) ` sets M"
diff -r 349c639e593c -r 7643b005b29a src/HOL/Probability/Information.thy
--- a/src/HOL/Probability/Information.thy	Sat Apr 14 20:19:52 2018 +0100
+++ b/src/HOL/Probability/Information.thy	Sun Apr 15 13:57:00 2018 +0100
@@ -834,9 +834,14 @@
     - log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX)"
     using Px Px_nn fin by (auto simp: measure_def)
   also have "- log b (\<integral> x. indicator {x \<in> space MX. Px x \<noteq> 0} x \<partial>MX) = - log b (\<integral> x. 1 / Px x \<partial>distr M MX X)"
-    unfolding distributed_distr_eq_density[OF X] using Px Px_nn
-    apply (intro arg_cong[where f="log b"] arg_cong[where f=uminus])
-    by (subst integral_density) (auto simp del: integral_indicator intro!: Bochner_Integration.integral_cong)
+  proof -
+    have "integral\<^sup>L MX (indicator {x \<in> space MX. Px x \<noteq> 0}) = LINT x|MX. Px x *\<^sub>R (1 / Px x)"
+      by (rule Bochner_Integration.integral_cong) auto
+    also have "... = LINT x|density MX (\<lambda>x. ennreal (Px x)). 1 / Px x"
+      by (rule integral_density [symmetric]) (use Px Px_nn in auto)
+    finally show ?thesis
+      unfolding distributed_distr_eq_density[OF X] by simp
+  qed
   also have "\<dots> \<le> (\<integral> x. - log b (1 / Px x) \<partial>distr M MX X)"
   proof (rule X.jensens_inequality[of "\<lambda>x. 1 / Px x" "{0<..}" 0 1 "\<lambda>x. - log b x"])
     show "AE x in distr M MX X. 1 / Px x \<in> {0<..}"