# HG changeset patch
# User paulson
# Date 1568298765 -3600
# Node ID 7e93a10b21f0f9c6654e56c9d6f19dbd7023f219
# Parent  086575316fd57a89753f92dfccc8c5a839fb7dd5# Parent  8518a750f7bb5b53744518d8932df4dbb40707db
merged

diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -2101,7 +2101,7 @@
   fixes p::real
   assumes [measurable]: "f \<in> borel_measurable M"
   shows "(\<lambda>x. \<bar>f x\<bar> powr p) \<in> borel_measurable M"
-unfolding powr_def by auto
+  by simp
 
 text \<open>The next one is a variation around \<open>measurable_restrict_space\<close>.\<close>
 
@@ -2115,6 +2115,12 @@
       measurable_restrict_space2[of f, of "restrict_space M A", of B, of N] assms(2) space_restrict_space)
 qed
 
+lemma measurable_restrict_mono:
+  assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
+  shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
+by (rule measurable_compose[OF measurable_restrict_space3 f])
+   (insert \<open>B \<subseteq> A\<close>, auto)
+
 text \<open>The next one is a variation around \<open>measurable_piecewise_restrict\<close>.\<close>
 
 lemma measurable_piecewise_restrict2:
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Analysis/Elementary_Normed_Spaces.thy
--- a/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Analysis/Elementary_Normed_Spaces.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -9,7 +9,7 @@
 theory Elementary_Normed_Spaces
   imports
   "HOL-Library.FuncSet"
-  Elementary_Metric_Spaces
+  Elementary_Metric_Spaces Linear_Algebra
   Connected
 begin
 
@@ -1100,34 +1100,6 @@
     by (simp add: fun_Compl_def uniformly_continuous_on_minus)
 
 
-subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological properties of linear functions\<close>
-
-lemma linear_lim_0:
-  assumes "bounded_linear f"
-  shows "(f \<longlongrightarrow> 0) (at (0))"
-proof -
-  interpret f: bounded_linear f by fact
-  have "(f \<longlongrightarrow> f 0) (at 0)"
-    using tendsto_ident_at by (rule f.tendsto)
-  then show ?thesis unfolding f.zero .
-qed
-
-lemma linear_continuous_at:
-  assumes "bounded_linear f"
-  shows "continuous (at a) f"
-  unfolding continuous_at using assms
-  apply (rule bounded_linear.tendsto)
-  apply (rule tendsto_ident_at)
-  done
-
-lemma linear_continuous_within:
-  "bounded_linear f \<Longrightarrow> continuous (at x within s) f"
-  using continuous_at_imp_continuous_within[of x f s] using linear_continuous_at[of f] by auto
-
-lemma linear_continuous_on:
-  "bounded_linear f \<Longrightarrow> continuous_on s f"
-  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
-
 subsection\<^marker>\<open>tag unimportant\<close> \<open>Arithmetic Preserves Topological Properties\<close>
 
 lemma open_scaling[intro]:
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy
--- a/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -4226,13 +4226,6 @@
 qed
 
 
-lemma borel_measurable_vimage_halfspace_component_lt:
-     "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-      (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_less])
-  apply (fastforce simp add: space_restrict_space)
-  done
-
 lemma borel_measurable_simple_function_limit:
   fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
   shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
@@ -4298,174 +4291,6 @@
     using borel_measurable_vimage_halfspace_component_lt by blast
 qed
 
-lemma borel_measurable_vimage_halfspace_component_ge:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_ge])
-  apply (fastforce simp add: space_restrict_space)
-  done
-
-lemma borel_measurable_vimage_halfspace_component_gt:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_greater])
-  apply (fastforce simp add: space_restrict_space)
-  done
-
-lemma borel_measurable_vimage_halfspace_component_le:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
-  apply (rule trans [OF borel_measurable_iff_halfspace_le])
-  apply (fastforce simp add: space_restrict_space)
-  done
-
-lemma
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows borel_measurable_vimage_open_interval:
-         "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S))" (is ?thesis1)
-   and borel_measurable_vimage_open:
-         "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>T. open T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))" (is ?thesis2)
-proof -
-  have "{x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" if "f \<in> borel_measurable (lebesgue_on S)" for a b
-  proof -
-    have "S = S \<inter> space lebesgue"
-      by simp
-    then have "S \<inter> (f -` box a b) \<in> sets (lebesgue_on S)"
-      by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that)
-    then show ?thesis
-      by (simp add: Collect_conj_eq vimage_def)
-  qed
-  moreover
-  have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
-       if T: "\<And>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" "open T" for T
-  proof -
-    obtain \<D> where "countable \<D>" and \<D>: "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = T"
-      using open_countable_Union_open_box that \<open>open T\<close> by metis
-    then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
-      by blast
-    have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
-      using that T \<D> by blast
-    then show ?thesis
-      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
-  qed
-  moreover
-  have eq: "{x \<in> S. f x \<bullet> i < a} = {x \<in> S. f x \<in> {y. y \<bullet> i < a}}" for i a
-    by auto
-  have "f \<in> borel_measurable (lebesgue_on S)"
-    if "\<And>T. open T \<Longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
-    by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that)
-  ultimately show "?thesis1" "?thesis2"
-    by blast+
-qed
-
-
-lemma borel_measurable_vimage_closed:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
-        (is "?lhs = ?rhs")
-proof -
-  have eq: "{x \<in> S. f x \<in> T} = S - {x \<in> S. f x \<in> (- T)}" for T
-    by auto
-  show ?thesis
-    apply (simp add: borel_measurable_vimage_open, safe)
-     apply (simp_all (no_asm) add: eq)
-     apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
-    apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
-    done
-qed
-
-lemma borel_measurable_vimage_closed_interval:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>a b. {x \<in> S. f x \<in> cbox a b} \<in> sets (lebesgue_on S))"
-        (is "?lhs = ?rhs")
-proof
-  assume ?lhs then show ?rhs
-    using borel_measurable_vimage_closed by blast
-next
-  assume RHS: ?rhs
-  have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)" if "open T" for T
-  proof -
-    obtain \<D> where "countable \<D>" and \<D>: "\<D> \<subseteq> Pow T" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = T"
-      using open_countable_Union_open_cbox that \<open>open T\<close> by metis
-    then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
-      by blast
-    have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
-      using that \<D> by (metis RHS)
-    then show ?thesis
-      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
-  qed
-  then show ?lhs
-    by (simp add: borel_measurable_vimage_open)
-qed
-
-lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
-  by auto
-
-lemma borel_measurable_vimage_borel:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
-         (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
-        (is "?lhs = ?rhs")
-proof
-  assume f: ?lhs
-  then show ?rhs
-    using measurable_sets [OF f]
-      by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def)
-qed (simp add: borel_measurable_vimage_open_interval)
-
-lemma lebesgue_measurable_vimage_borel:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "f \<in> borel_measurable lebesgue" "T \<in> sets borel"
-  shows "{x. f x \<in> T} \<in> sets lebesgue"
-  using assms borel_measurable_vimage_borel [of f UNIV] by auto
-
-lemma borel_measurable_if_I:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
-  shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
-proof -
-  have eq: "{x. x \<notin> S} \<union> {x. f x \<in> Y} = {x. x \<notin> S} \<union> {x. f x \<in> Y} \<inter> S" for Y
-    by blast
-  show ?thesis
-  using f S
-  apply (simp add: vimage_def in_borel_measurable_borel Ball_def)
-  apply (elim all_forward imp_forward asm_rl)
-  apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq)
-  apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff)
-  done
-qed
-
-lemma borel_measurable_if_D:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
-  shows "f \<in> borel_measurable (lebesgue_on S)"
-  using assms
-  apply (simp add: in_borel_measurable_borel Ball_def)
-  apply (elim all_forward imp_forward asm_rl)
-  apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
-  done
-
-lemma borel_measurable_if:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  assumes "S \<in> sets lebesgue"
-  shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
-  using assms borel_measurable_if_D borel_measurable_if_I by blast
-
-lemma borel_measurable_lebesgue_preimage_borel:
-  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
-  shows "f \<in> borel_measurable lebesgue \<longleftrightarrow>
-         (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
-  apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
-    apply (auto simp: in_borel_measurable_borel vimage_def)
-  done
-
 subsection \<open>Lebesgue sets and continuous images\<close>
 
 proposition lebesgue_regular_inner:
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -494,6 +494,11 @@
   shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x * c) has_integral (y * c)) S"
   using has_integral_linear[OF _ bounded_linear_mult_left] by (simp add: comp_def)
 
+lemma has_integral_divide:
+  fixes c :: "_ :: real_normed_div_algebra"
+  shows "(f has_integral y) S \<Longrightarrow> ((\<lambda>x. f x / c) has_integral (y / c)) S"
+  unfolding divide_inverse by (simp add: has_integral_mult_left)
+
 text\<open>The case analysis eliminates the condition \<^term>\<open>f integrable_on S\<close> at the cost
      of the type class constraint \<open>division_ring\<close>\<close>
 corollary integral_mult_left [simp]:
@@ -2735,6 +2740,34 @@
   shows "(\<lambda>x. x) integrable_on {a..b}"
 by (metis atLeastatMost_empty_iff integrable_on_def has_integral_empty ident_has_integral)
 
+lemma integral_sin [simp]:
+  fixes a::real
+  assumes "a \<le> b" shows "integral {a..b} sin = cos a - cos b"
+proof -
+  have "(sin has_integral (- cos b - - cos a)) {a..b}"
+  proof (rule fundamental_theorem_of_calculus)
+    show "((\<lambda>a. - cos a) has_vector_derivative sin x) (at x within {a..b})" for x
+      unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+      by (rule derivative_eq_intros | force)+
+  qed (use assms in auto)
+  then show ?thesis
+    by (simp add: integral_unique)
+qed
+
+lemma integral_cos [simp]:
+  fixes a::real
+  assumes "a \<le> b" shows "integral {a..b} cos = sin b - sin a"
+proof -
+  have "(cos has_integral (sin b - sin a)) {a..b}"
+  proof (rule fundamental_theorem_of_calculus)
+    show "(sin has_vector_derivative cos x) (at x within {a..b})" for x
+      unfolding has_field_derivative_iff_has_vector_derivative [symmetric]
+      by (rule derivative_eq_intros | force)+
+  qed (use assms in auto)
+  then show ?thesis
+    by (simp add: integral_unique)
+qed
+
 
 subsection \<open>Taylor series expansion\<close>
 
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Analysis/Lebesgue_Measure.thy
--- a/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Analysis/Lebesgue_Measure.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -462,8 +462,232 @@
   using integral_restrict_Int [of S UNIV f] assms
   by (simp add: lebesgue_on_UNIV_eq)
 
+lemma integrable_lebesgue_on_empty [iff]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{second_countable_topology,banach}"
+  shows "integrable (lebesgue_on {}) f"
+  by (simp add: integrable_restrict_space)
 
-text\<^marker>\<open>tag unimportant\<close> \<open>Measurability of continuous functions\<close>
+lemma integral_lebesgue_on_empty [simp]:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{second_countable_topology,banach}"
+  shows "integral\<^sup>L (lebesgue_on {}) f = 0"
+  by (simp add: Bochner_Integration.integral_empty)
+lemma has_bochner_integral_restrict_space:
+  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes \<Omega>: "\<Omega> \<inter> space M \<in> sets M"
+  shows "has_bochner_integral (restrict_space M \<Omega>) f i
+     \<longleftrightarrow> has_bochner_integral M (\<lambda>x. indicator \<Omega> x *\<^sub>R f x) i"
+  by (simp add: integrable_restrict_space [OF assms] integral_restrict_space [OF assms] has_bochner_integral_iff)
+
+lemma integrable_restrict_UNIV:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::{banach, second_countable_topology}"
+  assumes S: "S \<in> sets lebesgue"
+  shows  "integrable lebesgue (\<lambda>x. if x \<in> S then f x else 0) \<longleftrightarrow> integrable (lebesgue_on S) f"
+  using has_bochner_integral_restrict_space [of S lebesgue f] assms
+  by (simp add: integrable.simps indicator_scaleR_eq_if)
+
+lemma integral_mono_lebesgue_on_AE:
+  fixes f::"_ \<Rightarrow> real"
+  assumes f: "integrable (lebesgue_on T) f"
+    and gf: "AE x in (lebesgue_on S). g x \<le> f x"
+    and f0: "AE x in (lebesgue_on T). 0 \<le> f x"
+    and "S \<subseteq> T" and S: "S \<in> sets lebesgue" and T: "T \<in> sets lebesgue"
+  shows "(\<integral>x. g x \<partial>(lebesgue_on S)) \<le> (\<integral>x. f x \<partial>(lebesgue_on T))"
+proof -
+  have "(\<integral>x. g x \<partial>(lebesgue_on S)) = (\<integral>x. (if x \<in> S then g x else 0) \<partial>lebesgue)"
+    by (simp add: Lebesgue_Measure.integral_restrict_UNIV S)
+  also have "\<dots> \<le> (\<integral>x. (if x \<in> T then f x else 0) \<partial>lebesgue)"
+  proof (rule Bochner_Integration.integral_mono_AE')
+    show "integrable lebesgue (\<lambda>x. if x \<in> T then f x else 0)"
+      by (simp add: integrable_restrict_UNIV T f)
+    show "AE x in lebesgue. (if x \<in> S then g x else 0) \<le> (if x \<in> T then f x else 0)"
+      using assms by (auto simp: AE_restrict_space_iff)
+    show "AE x in lebesgue. 0 \<le> (if x \<in> T then f x else 0)"
+      using f0 by (simp add: AE_restrict_space_iff T)
+  qed
+  also have "\<dots> = (\<integral>x. f x \<partial>(lebesgue_on T))"
+    using Lebesgue_Measure.integral_restrict_UNIV T by blast
+  finally show ?thesis .
+qed
+
+
+subsection \<open>Borel measurability\<close>
+
+lemma borel_measurable_if_I:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes f: "f \<in> borel_measurable (lebesgue_on S)" and S: "S \<in> sets lebesgue"
+  shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
+proof -
+  have eq: "{x. x \<notin> S} \<union> {x. f x \<in> Y} = {x. x \<notin> S} \<union> {x. f x \<in> Y} \<inter> S" for Y
+    by blast
+  show ?thesis
+  using f S
+  apply (simp add: vimage_def in_borel_measurable_borel Ball_def)
+  apply (elim all_forward imp_forward asm_rl)
+  apply (simp only: Collect_conj_eq Collect_disj_eq imp_conv_disj eq)
+  apply (auto simp: Compl_eq [symmetric] Compl_in_sets_lebesgue sets_restrict_space_iff)
+  done
+qed
+
+lemma borel_measurable_if_D:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue"
+  shows "f \<in> borel_measurable (lebesgue_on S)"
+  using assms
+  apply (simp add: in_borel_measurable_borel Ball_def)
+  apply (elim all_forward imp_forward asm_rl)
+  apply (force simp: space_restrict_space sets_restrict_space image_iff intro: rev_bexI)
+  done
+
+lemma borel_measurable_if:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "S \<in> sets lebesgue"
+  shows "(\<lambda>x. if x \<in> S then f x else 0) \<in> borel_measurable lebesgue \<longleftrightarrow> f \<in> borel_measurable (lebesgue_on S)"
+  using assms borel_measurable_if_D borel_measurable_if_I by blast
+
+lemma borel_measurable_vimage_halfspace_component_lt:
+     "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+      (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i < a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_less])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma borel_measurable_vimage_halfspace_component_ge:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<ge> a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_ge])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma borel_measurable_vimage_halfspace_component_gt:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i > a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_greater])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma borel_measurable_vimage_halfspace_component_le:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a i. i \<in> Basis \<longrightarrow> {x \<in> S. f x \<bullet> i \<le> a} \<in> sets (lebesgue_on S))"
+  apply (rule trans [OF borel_measurable_iff_halfspace_le])
+  apply (fastforce simp add: space_restrict_space)
+  done
+
+lemma
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows borel_measurable_vimage_open_interval:
+         "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S))" (is ?thesis1)
+   and borel_measurable_vimage_open:
+         "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>T. open T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))" (is ?thesis2)
+proof -
+  have "{x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" if "f \<in> borel_measurable (lebesgue_on S)" for a b
+  proof -
+    have "S = S \<inter> space lebesgue"
+      by simp
+    then have "S \<inter> (f -` box a b) \<in> sets (lebesgue_on S)"
+      by (metis (no_types) box_borel in_borel_measurable_borel inf_sup_aci(1) space_restrict_space that)
+    then show ?thesis
+      by (simp add: Collect_conj_eq vimage_def)
+  qed
+  moreover
+  have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
+       if T: "\<And>a b. {x \<in> S. f x \<in> box a b} \<in> sets (lebesgue_on S)" "open T" for T
+  proof -
+    obtain \<D> where "countable \<D>" and \<D>: "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = box a b" "\<Union>\<D> = T"
+      using open_countable_Union_open_box that \<open>open T\<close> by metis
+    then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
+      by blast
+    have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
+      using that T \<D> by blast
+    then show ?thesis
+      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
+  qed
+  moreover
+  have eq: "{x \<in> S. f x \<bullet> i < a} = {x \<in> S. f x \<in> {y. y \<bullet> i < a}}" for i a
+    by auto
+  have "f \<in> borel_measurable (lebesgue_on S)"
+    if "\<And>T. open T \<Longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)"
+    by (metis (no_types) eq borel_measurable_vimage_halfspace_component_lt open_halfspace_component_lt that)
+  ultimately show "?thesis1" "?thesis2"
+    by blast+
+qed
+
+lemma borel_measurable_vimage_closed:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>T. closed T \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
+        (is "?lhs = ?rhs")
+proof -
+  have eq: "{x \<in> S. f x \<in> T} = S - {x \<in> S. f x \<in> (- T)}" for T
+    by auto
+  show ?thesis
+    apply (simp add: borel_measurable_vimage_open, safe)
+     apply (simp_all (no_asm) add: eq)
+     apply (intro sets.Diff sets_lebesgue_on_refl, force simp: closed_open)
+    apply (intro sets.Diff sets_lebesgue_on_refl, force simp: open_closed)
+    done
+qed
+
+lemma borel_measurable_vimage_closed_interval:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>a b. {x \<in> S. f x \<in> cbox a b} \<in> sets (lebesgue_on S))"
+        (is "?lhs = ?rhs")
+proof
+  assume ?lhs then show ?rhs
+    using borel_measurable_vimage_closed by blast
+next
+  assume RHS: ?rhs
+  have "{x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S)" if "open T" for T
+  proof -
+    obtain \<D> where "countable \<D>" and \<D>: "\<D> \<subseteq> Pow T" "\<And>X. X \<in> \<D> \<Longrightarrow> \<exists>a b. X = cbox a b" "\<Union>\<D> = T"
+      using open_countable_Union_open_cbox that \<open>open T\<close> by metis
+    then have eq: "{x \<in> S. f x \<in> T} = (\<Union>U \<in> \<D>. {x \<in> S. f x \<in> U})"
+      by blast
+    have "{x \<in> S. f x \<in> U} \<in> sets (lebesgue_on S)" if "U \<in> \<D>" for U
+      using that \<D> by (metis RHS)
+    then show ?thesis
+      by (auto simp: eq intro: Sigma_Algebra.sets.countable_UN' [OF \<open>countable \<D>\<close>])
+  qed
+  then show ?lhs
+    by (simp add: borel_measurable_vimage_open)
+qed
+
+lemma borel_measurable_UNIV_eq: "borel_measurable (lebesgue_on UNIV) = borel_measurable lebesgue"
+  by auto
+
+lemma borel_measurable_vimage_borel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
+         (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets (lebesgue_on S))"
+        (is "?lhs = ?rhs")
+proof
+  assume f: ?lhs
+  then show ?rhs
+    using measurable_sets [OF f]
+      by (simp add: Collect_conj_eq inf_sup_aci(1) space_restrict_space vimage_def)
+qed (simp add: borel_measurable_vimage_open_interval)
+
+lemma lebesgue_measurable_vimage_borel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  assumes "f \<in> borel_measurable lebesgue" "T \<in> sets borel"
+  shows "{x. f x \<in> T} \<in> sets lebesgue"
+  using assms borel_measurable_vimage_borel [of f UNIV] by auto
+
+lemma borel_measurable_lebesgue_preimage_borel:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
+  shows "f \<in> borel_measurable lebesgue \<longleftrightarrow>
+         (\<forall>T. T \<in> sets borel \<longrightarrow> {x. f x \<in> T} \<in> sets lebesgue)"
+  apply (intro iffI allI impI lebesgue_measurable_vimage_borel)
+    apply (auto simp: in_borel_measurable_borel vimage_def)
+  done
+
+
+subsection \<^marker>\<open>tag unimportant\<close> \<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"
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -1879,4 +1879,88 @@
         orthogonal_commute orthogonal_def)
 qed
 
+subsection\<open>Linear functions are (uniformly) continuous on any set\<close>
+
+subsection\<^marker>\<open>tag unimportant\<close> \<open>Topological properties of linear functions\<close>
+
+lemma linear_lim_0:
+  assumes "bounded_linear f"
+  shows "(f \<longlongrightarrow> 0) (at (0))"
+proof -
+  interpret f: bounded_linear f by fact
+  have "(f \<longlongrightarrow> f 0) (at 0)"
+    using tendsto_ident_at by (rule f.tendsto)
+  then show ?thesis unfolding f.zero .
+qed
+
+lemma linear_continuous_at:
+  assumes "bounded_linear f"
+  shows "continuous (at a) f"
+  unfolding continuous_at using assms
+  apply (rule bounded_linear.tendsto)
+  apply (rule tendsto_ident_at)
+  done
+
+lemma linear_continuous_within:
+  "bounded_linear f \<Longrightarrow> continuous (at x within s) f"
+  using continuous_at_imp_continuous_at_within linear_continuous_at by blast
+
+lemma linear_continuous_on:
+  "bounded_linear f \<Longrightarrow> continuous_on s f"
+  using continuous_at_imp_continuous_on[of s f] using linear_continuous_at[of f] by auto
+
+lemma Lim_linear:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and h :: "'b \<Rightarrow> 'c::real_normed_vector"
+  assumes "(f \<longlongrightarrow> l) F" "linear h"
+  shows "((\<lambda>x. h(f x)) \<longlongrightarrow> h l) F"
+proof -
+  obtain B where B: "B > 0" "\<And>x. norm (h x) \<le> B * norm x"
+    using linear_bounded_pos [OF \<open>linear h\<close>] by blast
+  show ?thesis
+    unfolding tendsto_iff
+  proof (intro allI impI)
+    show "\<forall>\<^sub>F x in F. dist (h (f x)) (h l) < e" if "e > 0" for e
+    proof -
+      have "\<forall>\<^sub>F x in F. dist (f x) l < e/B"
+        by (simp add: \<open>0 < B\<close> assms(1) tendstoD that)
+      then show ?thesis
+        unfolding dist_norm
+      proof (rule eventually_mono)
+        show "norm (h (f x) - h l) < e" if "norm (f x - l) < e / B" for x
+          using that B
+          apply (simp add: divide_simps)
+          by (metis \<open>linear h\<close> le_less_trans linear_diff mult.commute)
+      qed
+    qed
+  qed
+qed
+
+lemma linear_continuous_compose:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and g :: "'b \<Rightarrow> 'c::real_normed_vector"
+  assumes "continuous F f" "linear g"
+  shows "continuous F (\<lambda>x. g(f x))"
+  using assms unfolding continuous_def by (rule Lim_linear)
+
+lemma linear_continuous_on_compose:
+  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space" and g :: "'b \<Rightarrow> 'c::real_normed_vector"
+  assumes "continuous_on S f" "linear g"
+  shows "continuous_on S (\<lambda>x. g(f x))"
+  using assms by (simp add: continuous_on_eq_continuous_within linear_continuous_compose)
+
+text\<open>Also bilinear functions, in composition form\<close>
+
+lemma bilinear_continuous_compose:
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+  assumes "continuous F f" "continuous F g" "bilinear h"
+  shows "continuous F (\<lambda>x. h (f x) (g x))"
+  using assms bilinear_conv_bounded_bilinear bounded_bilinear.continuous by blast
+
+lemma bilinear_continuous_on_compose:
+  fixes h :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space \<Rightarrow> 'c::real_normed_vector"
+    and f :: "'d::t2_space \<Rightarrow> 'a"
+  assumes "continuous_on S f" "continuous_on S g" "bilinear h"
+  shows "continuous_on S (\<lambda>x. h (f x) (g x))"
+  using assms by (simp add: continuous_on_eq_continuous_within bilinear_continuous_compose)
+
+
 end
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Library/Landau_Symbols.thy
--- a/src/HOL/Library/Landau_Symbols.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Library/Landau_Symbols.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -1641,10 +1641,6 @@
 
 subsection \<open>Asymptotic Equivalence\<close>
 
-(* TODO Move *)
-lemma tendsto_eventually: "eventually (\<lambda>x. f x = c) F \<Longrightarrow> filterlim f (nhds c) F"
-  by (simp add: eventually_mono eventually_nhds_x_imp_x filterlim_iff)
-
 named_theorems asymp_equiv_intros
 named_theorems asymp_equiv_simps
 
@@ -1676,7 +1672,7 @@
     by (intro always_eventually) simp
   moreover have "((\<lambda>_. 1) \<longlongrightarrow> 1) F" by simp
   ultimately show "((\<lambda>x. if f x = 0 \<and> f x = 0 then 1 else f x / f x) \<longlongrightarrow> 1) F"
-    by (simp add: Landau_Symbols.tendsto_eventually)
+    by (simp add: tendsto_eventually)
 qed
 
 lemma asymp_equiv_symI: 
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Limits.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -779,6 +779,14 @@
   for c :: "'a::topological_semigroup_mult"
   by (rule tendsto_mult [OF _ tendsto_const])
 
+lemma real_tendsto_mult_left_iff:
+   "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. c * f x) (c * l) F \<longleftrightarrow> tendsto f l F" for c :: real
+  by (auto simp: tendsto_mult_left dest: tendsto_mult_left [where c = "1/c"])
+
+lemma real_tendsto_mult_right_iff:
+   "c \<noteq> 0 \<Longrightarrow> tendsto(\<lambda>x. f x * c) (l * c) F \<longleftrightarrow> tendsto f l F" for c :: real
+  by (simp add: mult.commute real_tendsto_mult_left_iff)
+
 lemma lim_const_over_n [tendsto_intros]:
   fixes a :: "'a::real_normed_field"
   shows "(\<lambda>n. a / of_nat n) \<longlonglongrightarrow> 0"
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Power.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -895,6 +895,11 @@
   apply simp
   done
 
+lemma dvd_power_iff_le:
+  fixes k::nat
+  shows "2 \<le> k \<Longrightarrow> ((k ^ m) dvd (k ^ n) \<longleftrightarrow> m \<le> n)"
+  using le_imp_power_dvd power_dvd_imp_le by force
+
 lemma power2_nat_le_eq_le: "m\<^sup>2 \<le> n\<^sup>2 \<longleftrightarrow> m \<le> n"
   for m n :: nat
   by (auto intro: power2_le_imp_le power_mono)
diff -r 086575316fd5 -r 7e93a10b21f0 src/HOL/Probability/Tree_Space.thy
--- a/src/HOL/Probability/Tree_Space.thy	Thu Sep 12 16:21:44 2019 +0200
+++ b/src/HOL/Probability/Tree_Space.thy	Thu Sep 12 15:32:45 2019 +0100
@@ -247,13 +247,6 @@
     by (auto simp: sets_restrict_space_iff space_restrict_space)
 qed
 
-lemma measurable_restrict_mono:
-  assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
-  shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
-by (rule measurable_compose[OF measurable_restrict_space3 f])
-   (insert \<open>B \<subseteq> A\<close>, auto)
-
-
 lemma measurable_value[measurable (raw)]:
   assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
     and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"