# HG changeset patch
# User immler
# Date 1519309045 -3600
# Node ID bdff8bf0a75bff999eaccd5ed2ae1f913f0b23bf
# Parent  00c43648839802ef0899ecd019427a0e6d7ac719
moved theorems from AFP/Affine_Arithmetic and AFP/Ordinary_Differential_Equations

diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Borel_Space.thy
--- a/src/HOL/Analysis/Borel_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Borel_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -242,6 +242,11 @@
   shows "S \<noteq> {} \<Longrightarrow> bdd_above S \<Longrightarrow> closed S \<Longrightarrow> Sup S \<in> S"
   by (subst closure_closed[symmetric], assumption, rule closure_contains_Sup)
 
+lemma closed_subset_contains_Sup:
+  fixes A C :: "real set"
+  shows "closed C \<Longrightarrow> A \<subseteq> C \<Longrightarrow> A \<noteq> {} \<Longrightarrow> bdd_above A \<Longrightarrow> Sup A \<in> C"
+  by (metis closure_contains_Sup closure_minimal subset_eq)
+
 lemma deriv_nonneg_imp_mono:
   assumes deriv: "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_real_derivative g' x) (at x)"
   assumes nonneg: "\<And>x. x \<in> {a..b} \<Longrightarrow> g' x \<ge> 0"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -8,8 +8,35 @@
 imports
   Topology_Euclidean_Space
   Operator_Norm
+  Uniform_Limit
 begin
 
+lemma onorm_componentwise:
+  assumes "bounded_linear f"
+  shows "onorm f \<le> (\<Sum>i\<in>Basis. norm (f i))"
+proof -
+  {
+    fix i::'a
+    assume "i \<in> Basis"
+    hence "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> onorm (\<lambda>x. (x \<bullet> i)) * norm (f i)"
+      by (auto intro!: onorm_scaleR_left_lemma bounded_linear_inner_left)
+    also have "\<dots> \<le>  norm i * norm (f i)"
+      by (rule mult_right_mono)
+        (auto simp: ac_simps Cauchy_Schwarz_ineq2 intro!: onorm_le)
+    finally have "onorm (\<lambda>x. (x \<bullet> i) *\<^sub>R f i) \<le> norm (f i)" using \<open>i \<in> Basis\<close>
+      by simp
+  } hence "onorm (\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) \<le> (\<Sum>i\<in>Basis. norm (f i))"
+    by (auto intro!: order_trans[OF onorm_sum_le] bounded_linear_scaleR_const
+      sum_mono bounded_linear_inner_left)
+  also have "(\<lambda>x. \<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R f i) = (\<lambda>x. f (\<Sum>i\<in>Basis. (x \<bullet> i) *\<^sub>R i))"
+    by (simp add: linear_sum bounded_linear.linear assms linear_simps)
+  also have "\<dots> = f"
+    by (simp add: euclidean_representation)
+  finally show ?thesis .
+qed
+
+lemmas onorm_componentwise_le = order_trans[OF onorm_componentwise]
+
 subsection \<open>Intro rules for @{term bounded_linear}\<close>
 
 named_theorems bounded_linear_intros
@@ -447,6 +474,15 @@
   shows "continuous F f"
   using assms by (auto simp: continuous_def intro!: tendsto_componentwise1)
 
+lemma
+  continuous_on_blinfun_componentwise:
+  fixes f:: "'d::t2_space \<Rightarrow> 'e::euclidean_space \<Rightarrow>\<^sub>L 'f::real_normed_vector"
+  assumes "\<And>i. i \<in> Basis \<Longrightarrow> continuous_on s (\<lambda>x. f x i)"
+  shows "continuous_on s f"
+  using assms
+  by (auto intro!: continuous_at_imp_continuous_on intro!: tendsto_componentwise1
+    simp: continuous_on_eq_continuous_within continuous_def)
+
 lemma bounded_linear_blinfun_matrix: "bounded_linear (\<lambda>x. (x::_\<Rightarrow>\<^sub>L _) j \<bullet> i)"
   by (auto intro!: bounded_linearI' bounded_linear_intros)
 
@@ -692,4 +728,9 @@
 lemma bounded_linear_blinfun_mult_left[bounded_linear]: "bounded_linear blinfun_mult_left"
   by transfer (rule bounded_bilinear.flip[OF bounded_bilinear_mult])
 
+lemmas bounded_linear_function_uniform_limit_intros[uniform_limit_intros] =
+  bounded_linear.uniform_limit[OF bounded_linear_apply_blinfun]
+  bounded_linear.uniform_limit[OF bounded_linear_blinfun_apply]
+  bounded_linear.uniform_limit[OF bounded_linear_blinfun_matrix]
+
 end
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -1,7 +1,7 @@
 section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space.\<close>
 
 theory Cartesian_Euclidean_Space
-imports Finite_Cartesian_Product Derivative 
+imports Finite_Cartesian_Product Derivative
 begin
 
 lemma subspace_special_hyperplane: "subspace {x. x $ k = 0}"
@@ -1455,4 +1455,9 @@
   unfolding vec_lambda_beta
   by auto
 
+lemmas cartesian_euclidean_space_uniform_limit_intros[uniform_limit_intros] =
+  bounded_linear.uniform_limit[OF blinfun.bounded_linear_right]
+  bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
+  bounded_linear.uniform_limit[OF bounded_linear_component_cart]
+
 end
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Cauchy_Integral_Theorem.thy
--- a/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Cauchy_Integral_Theorem.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -1199,7 +1199,7 @@
 
 lemma vector_derivative_linepath_within:
     "x \<in> {0..1} \<Longrightarrow> vector_derivative (linepath a b) (at x within {0..1}) = b - a"
-  apply (rule vector_derivative_within_closed_interval [of 0 "1::real", simplified])
+  apply (rule vector_derivative_within_cbox [of 0 "1::real", simplified])
   apply (auto simp: has_vector_derivative_linepath_within)
   done
 
@@ -2695,7 +2695,7 @@
   then have *: "(\<lambda>y. (?pathint x y - f x * (y - x)) /\<^sub>R cmod (y - x)) \<midarrow>x\<rightarrow> 0"
     by (simp add: Lim_at dist_norm inverse_eq_divide)
   show ?thesis
-    apply (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right)
+    apply (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right)
     apply (rule Lim_transform [OF * Lim_eventually])
     apply (simp add: inverse_eq_divide [symmetric] eventually_at)
     using \<open>open s\<close> x
@@ -3573,7 +3573,7 @@
       if "x \<in> {0..1} - S" for x
     proof -
       have "vector_derivative (uminus \<circ> \<gamma>) (at x within cbox 0 1) = - vector_derivative \<gamma> (at x within cbox 0 1)"
-        apply (rule vector_derivative_within_closed_interval)
+        apply (rule vector_derivative_within_cbox)
         using that
           apply (auto simp: o_def)
         apply (rule has_vector_derivative_minus)
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -1095,6 +1095,43 @@
   qed
 qed
 
+text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
+
+lemma distance_attains_sup:
+  assumes "compact s" "s \<noteq> {}"
+  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
+proof (rule continuous_attains_sup [OF assms])
+  {
+    fix x
+    assume "x\<in>s"
+    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
+      by (intro tendsto_dist tendsto_const tendsto_ident_at)
+  }
+  then show "continuous_on s (dist a)"
+    unfolding continuous_on ..
+qed
+
+text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
+
+lemma distance_attains_inf:
+  fixes a :: "'a::heine_borel"
+  assumes "closed s" and "s \<noteq> {}"
+  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
+proof -
+  from assms obtain b where "b \<in> s" by auto
+  let ?B = "s \<inter> cball a (dist b a)"
+  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
+    by (auto simp: dist_commute)
+  moreover have "continuous_on ?B (dist a)"
+    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
+  moreover have "compact ?B"
+    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
+  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
+    by (metis continuous_attains_inf)
+  with that show ?thesis by fastforce
+qed
+
+
 subsection\<open>Relations among convergence and absolute convergence for power series.\<close>
 
 lemma summable_imp_bounded:
@@ -1353,6 +1390,24 @@
   shows "infdist x S > 0"
 using in_closed_iff_infdist_zero[OF assms(1) assms(2), of x] assms(3) infdist_nonneg le_less by fastforce
 
+lemma
+  infdist_attains_inf:
+  fixes X::"'a::heine_borel set"
+  assumes "closed X"
+  assumes "X \<noteq> {}"
+  obtains x where "x \<in> X" "infdist y X = dist y x"
+proof -
+  have "bdd_below (dist y ` X)"
+    by auto
+  from distance_attains_inf[OF assms, of y]
+  obtain x where INF: "x \<in> X" "\<And>z. z \<in> X \<Longrightarrow> dist y x \<le> dist y z" by auto
+  have "infdist y X = dist y x"
+    by (auto simp: infdist_def assms
+      intro!: antisym cINF_lower[OF _ \<open>x \<in> X\<close>] cINF_greatest[OF assms(2) INF(2)])
+  with \<open>x \<in> X\<close> show ?thesis ..
+qed
+
+
 text \<open>Every metric space is a T4 space:\<close>
 
 instance metric_space \<subseteq> t4_space
@@ -1423,6 +1478,36 @@
   shows "continuous F (\<lambda>x. infdist (f x) A)"
   using assms unfolding continuous_def by (rule tendsto_infdist)
 
+lemma compact_infdist_le:
+  fixes A::"'a::heine_borel set"
+  assumes "A \<noteq> {}"
+  assumes "compact A"
+  assumes "e > 0"
+  shows "compact {x. infdist x A \<le> e}"
+proof -
+  from continuous_closed_vimage[of "{0..e}" "\<lambda>x. infdist x A"]
+    continuous_infdist[OF continuous_ident, of _ UNIV A]
+  have "closed {x. infdist x A \<le> e}" by (auto simp: vimage_def infdist_nonneg)
+  moreover
+  from assms obtain x0 b where b: "\<And>x. x \<in> A \<Longrightarrow> dist x0 x \<le> b" "closed A"
+    by (auto simp: compact_eq_bounded_closed bounded_def)
+  {
+    fix y
+    assume le: "infdist y A \<le> e"
+    from infdist_attains_inf[OF \<open>closed A\<close> \<open>A \<noteq> {}\<close>, of y]
+    obtain z where z: "z \<in> A" "infdist y A = dist y z" by blast
+    have "dist x0 y \<le> dist y z + dist x0 z"
+      by (metis dist_commute dist_triangle)
+    also have "dist y z \<le> e" using le z by simp
+    also have "dist x0 z \<le> b" using b z by simp
+    finally have "dist x0 y \<le> b + e" by arith
+  } then
+  have "bounded {x. infdist x A \<le> e}"
+    by (auto simp: bounded_any_center[where a=x0] intro!: exI[where x="b + e"])
+  ultimately show "compact {x. infdist x A \<le> e}"
+    by (simp add: compact_eq_bounded_closed)
+qed
+
 subsection \<open>Equality of continuous functions on closure and related results.\<close>
 
 lemma continuous_closedin_preimage_constant:
@@ -2209,6 +2294,13 @@
     by (metis assms continuous_open_vimage vimage_def)
 qed
 
+lemma open_neg_translation:
+  fixes s :: "'a::real_normed_vector set"
+  assumes "open s"
+  shows "open((\<lambda>x. a - x) ` s)"
+  using open_translation[OF open_negations[OF assms], of a]
+  by (auto simp: image_image)
+
 lemma open_affinity:
   fixes S :: "'a::real_normed_vector set"
   assumes "open S"  "c \<noteq> 0"
@@ -2392,42 +2484,6 @@
     (\<forall>x \<in> s. \<forall>e>0. \<exists>d>0. (\<forall>x' \<in> s. norm(x' - x) < d \<longrightarrow> \<bar>f x' - f x\<bar> < e))"
   unfolding continuous_on_iff dist_norm by simp
 
-text \<open>Hence some handy theorems on distance, diameter etc. of/from a set.\<close>
-
-lemma distance_attains_sup:
-  assumes "compact s" "s \<noteq> {}"
-  shows "\<exists>x\<in>s. \<forall>y\<in>s. dist a y \<le> dist a x"
-proof (rule continuous_attains_sup [OF assms])
-  {
-    fix x
-    assume "x\<in>s"
-    have "(dist a \<longlongrightarrow> dist a x) (at x within s)"
-      by (intro tendsto_dist tendsto_const tendsto_ident_at)
-  }
-  then show "continuous_on s (dist a)"
-    unfolding continuous_on ..
-qed
-
-text \<open>For \emph{minimal} distance, we only need closure, not compactness.\<close>
-
-lemma distance_attains_inf:
-  fixes a :: "'a::heine_borel"
-  assumes "closed s" and "s \<noteq> {}"
-  obtains x where "x\<in>s" "\<And>y. y \<in> s \<Longrightarrow> dist a x \<le> dist a y"
-proof -
-  from assms obtain b where "b \<in> s" by auto
-  let ?B = "s \<inter> cball a (dist b a)"
-  have "?B \<noteq> {}" using \<open>b \<in> s\<close>
-    by (auto simp: dist_commute)
-  moreover have "continuous_on ?B (dist a)"
-    by (auto intro!: continuous_at_imp_continuous_on continuous_dist continuous_ident continuous_const)
-  moreover have "compact ?B"
-    by (intro closed_Int_compact \<open>closed s\<close> compact_cball)
-  ultimately obtain x where "x \<in> ?B" "\<forall>y\<in>?B. dist a x \<le> dist a y"
-    by (metis continuous_attains_inf)
-  with that show ?thesis by fastforce
-qed
-
 
 subsection \<open>Cartesian products\<close>
 
@@ -2911,6 +2967,38 @@
     using separate_compact_closed[OF assms(2,1) *] by (force simp: dist_commute)
 qed
 
+lemma compact_in_open_separated:
+  fixes A::"'a::heine_borel set"
+  assumes "A \<noteq> {}"
+  assumes "compact A"
+  assumes "open B"
+  assumes "A \<subseteq> B"
+  obtains e where "e > 0" "{x. infdist x A \<le> e} \<subseteq> B"
+proof atomize_elim
+  have "closed (- B)" "compact A" "- B \<inter> A = {}"
+    using assms by (auto simp: open_Diff compact_eq_bounded_closed)
+  from separate_closed_compact[OF this]
+  obtain d'::real where d': "d'>0" "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d' \<le> dist x y"
+    by auto
+  define d where "d = d' / 2"
+  hence "d>0" "d < d'" using d' by auto
+  with d' have d: "\<And>x y. x \<notin> B \<Longrightarrow> y \<in> A \<Longrightarrow> d < dist x y"
+    by force
+  show "\<exists>e>0. {x. infdist x A \<le> e} \<subseteq> B"
+  proof (rule ccontr)
+    assume "\<nexists>e. 0 < e \<and> {x. infdist x A \<le> e} \<subseteq> B"
+    with \<open>d > 0\<close> obtain x where x: "infdist x A \<le> d" "x \<notin> B"
+      by auto
+    from assms have "closed A" "A \<noteq> {}" by (auto simp: compact_eq_bounded_closed)
+    from infdist_attains_inf[OF this]
+    obtain y where y: "y \<in> A" "infdist x A = dist x y"
+      by auto
+    have "dist x y \<le> d" using x y by simp
+    also have "\<dots> < dist x y" using y d x by auto
+    finally show False by simp
+  qed
+qed
+
 
 subsection \<open>Compact sets and the closure operation.\<close>
 
@@ -4221,6 +4309,14 @@
     using \<open>x\<in>s\<close> by blast
 qed
 
+lemma banach_fix_type:
+  fixes f::"'a::complete_space\<Rightarrow>'a"
+  assumes c:"0 \<le> c" "c < 1"
+      and lipschitz:"\<forall>x. \<forall>y. dist (f x) (f y) \<le> c * dist x y"
+  shows "\<exists>!x. (f x = x)"
+  using assms banach_fix[OF complete_UNIV UNIV_not_empty assms(1,2) subset_UNIV, of f]
+  by auto
+
 
 subsection \<open>Edelstein fixed point theorem\<close>
 
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Convex_Euclidean_Space.thy
--- a/src/HOL/Analysis/Convex_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Convex_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -6659,9 +6659,13 @@
 
 subsection \<open>On \<open>real\<close>, \<open>is_interval\<close>, \<open>convex\<close> and \<open>connected\<close> are all equivalent.\<close>
 
-lemma is_interval_1:
-  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
-  unfolding is_interval_def by auto
+lemma mem_is_interval_1_I:
+  fixes a b c::real
+  assumes "is_interval S"
+  assumes "a \<in> S" "c \<in> S"
+  assumes "a \<le> b" "b \<le> c"
+  shows "b \<in> S"
+  using assms is_interval_1 by blast
 
 lemma is_interval_connected_1:
   fixes s :: "real set"
@@ -6708,6 +6712,9 @@
   shows "is_interval s \<longleftrightarrow> convex s"
   by (metis is_interval_convex convex_connected is_interval_connected_1)
 
+lemma is_interval_ball_real: "is_interval (ball a b)" for a b::real
+  by (metis connected_ball is_interval_connected_1)
+
 lemma connected_compact_interval_1:
      "connected S \<and> compact S \<longleftrightarrow> (\<exists>a b. S = {a..b::real})"
   by (auto simp: is_interval_connected_1 [symmetric] is_interval_compact)
@@ -6731,6 +6738,10 @@
     by (metis connected_convex_1 convex_linear_vimage linf convex_connected connected_linear_image)
 qed
 
+lemma is_interval_cball_1[intro, simp]: "is_interval (cball a b)" for a b::real
+  by (auto simp: is_interval_convex_1 convex_cball)
+
+
 subsection \<open>Another intermediate value theorem formulation\<close>
 
 lemma ivt_increasing_component_on_1:
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Derivative.thy
--- a/src/HOL/Analysis/Derivative.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Derivative.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -48,18 +48,6 @@
   shows "((\<lambda>x. h (f x) (g x)) has_derivative (\<lambda>d. h (f x) (g' d) + h (f' d) (g x))) (at x)"
   using has_derivative_bilinear_within[of f f' x UNIV g g' h] assms by simp
 
-text \<open>These are the only cases we'll care about, probably.\<close>
-
-lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
-    bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
-  unfolding has_derivative_def Lim
-  by (auto simp add: netlimit_within field_simps)
-
-lemma has_derivative_at: "(f has_derivative f') (at x) \<longleftrightarrow>
-    bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
-  using has_derivative_within [of f f' x UNIV]
-  by simp
-
 text \<open>More explicit epsilon-delta forms.\<close>
 
 lemma has_derivative_within':
@@ -131,27 +119,6 @@
     by (auto simp add: continuous_within DERIV_within_iff cong: Lim_cong_within)
 qed
 
-subsubsection \<open>Limit transformation for derivatives\<close>
-
-lemma has_derivative_transform_within:
-  assumes "(f has_derivative f') (at x within s)"
-    and "0 < d"
-    and "x \<in> s"
-    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
-  shows "(g has_derivative f') (at x within s)"
-  using assms
-  unfolding has_derivative_within
-  by (force simp add: intro: Lim_transform_within)
-
-lemma has_derivative_transform_within_open:
-  assumes "(f has_derivative f') (at x)"
-    and "open s"
-    and "x \<in> s"
-    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
-  shows "(g has_derivative f') (at x)"
-  using assms  unfolding has_derivative_at
-  by (force simp add: intro: Lim_transform_within_open)
-
 subsection \<open>Differentiability\<close>
 
 definition
@@ -304,6 +271,10 @@
   unfolding differentiable_on_def
   by auto
 
+lemma has_derivative_continuous_on:
+  "(\<And>x. x \<in> s \<Longrightarrow> (f has_derivative f' x) (at x within s)) \<Longrightarrow> continuous_on s f"
+  by (auto intro!: differentiable_imp_continuous_on differentiableI simp: differentiable_on_def)
+
 text \<open>Results about neighborhoods filter.\<close>
 
 lemma eventually_nhds_metric_le:
@@ -1143,6 +1114,20 @@
     by (simp add: g_def field_simps linear_diff[OF has_derivative_linear[OF f']])
 qed
 
+lemma vector_differentiable_bound_linearization:
+  fixes f::"real \<Rightarrow> 'b::real_normed_vector"
+  assumes f': "\<And>x. x \<in> S \<Longrightarrow> (f has_vector_derivative f' x) (at x within S)"
+  assumes "closed_segment a b \<subseteq> S"
+  assumes B: "\<forall>x\<in>S. norm (f' x - f' x0) \<le> B"
+  assumes "x0 \<in> S"
+  shows "norm (f b - f a - (b - a) *\<^sub>R f' x0) \<le> norm (b - a) * B"
+  using assms
+  by (intro differentiable_bound_linearization[of a b S f "\<lambda>x h. h *\<^sub>R f' x" x0 B])
+    (force simp: closed_segment_real_eq has_vector_derivative_def
+      scaleR_diff_right[symmetric] mult.commute[of B]
+      intro!: onorm_le mult_left_mono)+
+
+
 text \<open>In particular.\<close>
 
 lemma has_derivative_zero_constant:
@@ -1169,6 +1154,14 @@
     using assms(2)[of x] by (simp add: has_field_derivative_def A)
 qed fact
 
+lemma
+  has_vector_derivative_zero_constant:
+  assumes "convex s"
+  assumes "\<And>x. x \<in> s \<Longrightarrow> (f has_vector_derivative 0) (at x within s)"
+  obtains c where "\<And>x. x \<in> s \<Longrightarrow> f x = c"
+  using has_derivative_zero_constant[of s f] assms
+  by (auto simp: has_vector_derivative_def)
+
 lemma has_derivative_zero_unique:
   fixes f :: "'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector"
   assumes "convex s"
@@ -2510,7 +2503,7 @@
 apply (auto simp: vector_derivative_works has_vector_derivative_def has_field_derivative_def mult_commute_abs)
 done
 
-lemma vector_derivative_within_closed_interval:
+lemma vector_derivative_within_cbox:
   assumes ab: "a < b" "x \<in> cbox a b"
   assumes f: "(f has_vector_derivative f') (at x within cbox a b)"
   shows "vector_derivative f (at x within cbox a b) = f'"
@@ -2518,6 +2511,14 @@
             vector_derivative_works[THEN iffD1] differentiableI_vector)
      fact
 
+lemma vector_derivative_within_closed_interval:
+  fixes f::"real \<Rightarrow> 'a::euclidean_space"
+  assumes "a < b" and "x \<in> {a .. b}"
+  assumes "(f has_vector_derivative f') (at x within {a .. b})"
+  shows "vector_derivative f (at x within {a .. b}) = f'"
+  using assms vector_derivative_within_cbox
+  by fastforce
+
 lemma has_vector_derivative_within_subset:
   "(f has_vector_derivative f') (at x within s) \<Longrightarrow> t \<subseteq> s \<Longrightarrow> (f has_vector_derivative f') (at x within t)"
   by (auto simp: has_vector_derivative_def intro: has_derivative_within_subset)
@@ -2561,6 +2562,14 @@
   unfolding has_vector_derivative_def
   by (rule has_derivative_transform_within_open)
 
+lemma has_vector_derivative_transform:
+  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+  assumes f': "(f has_vector_derivative f') (at x within s)"
+  shows "(g has_vector_derivative f') (at x within s)"
+  using assms
+  unfolding has_vector_derivative_def
+  by (rule has_derivative_transform)
+
 lemma vector_diff_chain_at:
   assumes "(f has_vector_derivative f') (at x)"
     and "(g has_vector_derivative g') (at (f x))"
@@ -2589,7 +2598,7 @@
 lemma vector_derivative_at_within_ivl:
   "(f has_vector_derivative f') (at x) \<Longrightarrow>
     a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> a<b \<Longrightarrow> vector_derivative f (at x within {a..b}) = f'"
-using has_vector_derivative_at_within vector_derivative_within_closed_interval by fastforce
+  using has_vector_derivative_at_within vector_derivative_within_cbox by fastforce
 
 lemma vector_derivative_chain_at:
   assumes "f differentiable at x" "(g differentiable at (f x))"
@@ -2917,21 +2926,19 @@
 qed
 
 lemma has_derivative_partialsI:
-  assumes fx: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>x. f x y) has_derivative blinfun_apply (fx x y)) (at x within X)"
+  fixes f::"'a::real_normed_vector \<Rightarrow> 'b::real_normed_vector \<Rightarrow> 'c::real_normed_vector"
+  assumes fx: "((\<lambda>x. f x y) has_derivative fx) (at x within X)"
   assumes fy: "\<And>x y. x \<in> X \<Longrightarrow> y \<in> Y \<Longrightarrow> ((\<lambda>y. f x y) has_derivative blinfun_apply (fy x y)) (at y within Y)"
-  assumes fx_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fx x y)"
-  assumes fy_cont: "continuous_on (X \<times> Y) (\<lambda>(x, y). fy x y)"
-  assumes "x \<in> X" "y \<in> Y"
-  assumes "convex X" "convex Y"
-  shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx x y tx + fy x y ty)) (at (x, y) within X \<times> Y)"
+  assumes fy_cont[unfolded continuous_within]: "continuous (at (x, y) within X \<times> Y) (\<lambda>(x, y). fy x y)"
+  assumes "y \<in> Y" "convex Y"
+  shows "((\<lambda>(x, y). f x y) has_derivative (\<lambda>(tx, ty). fx tx + fy x y ty)) (at (x, y) within X \<times> Y)"
 proof (safe intro!: has_derivativeI tendstoI, goal_cases)
   case (2 e')
+  interpret fx: bounded_linear "fx" using fx by (rule has_derivative_bounded_linear)
   define e where "e = e' / 9"
   have "e > 0" using \<open>e' > 0\<close> by (simp add: e_def)
 
-  have "(x, y) \<in> X \<times> Y" using assms by auto
-  from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF this,
-    unfolded continuous_within, THEN tendstoD, OF \<open>e > 0\<close>]
+  from fy_cont[THEN tendstoD, OF \<open>e > 0\<close>]
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. dist (fy x' y') (fy x y) < e"
     by (auto simp: split_beta')
   from this[unfolded eventually_at] obtain d' where
@@ -2971,12 +2978,12 @@
   } note onorm = this
 
   have ev_mem: "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. (x', y') \<in> X \<times> Y"
-    using \<open>x \<in> X\<close> \<open>y \<in> Y\<close>
+    using \<open>y \<in> Y\<close>
     by (auto simp: eventually_at intro!: zero_less_one)
   moreover
   have ev_dist: "\<forall>\<^sub>F xy in at (x, y) within X \<times> Y. dist xy (x, y) < d" if "d > 0" for d
     using eventually_at_ball[OF that]
-    by (rule eventually_elim2) (auto simp: dist_commute intro!: eventually_True)
+    by (rule eventually_elim2) (auto simp: dist_commute mem_ball intro!: eventually_True)
   note ev_dist[OF \<open>0 < d\<close>]
   ultimately
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
@@ -2997,32 +3004,31 @@
       have "\<dots> \<subseteq> ball y d \<inter> Y"
         using \<open>y \<in> Y\<close> \<open>0 < d\<close> dy y'
         by (intro \<open>convex ?S\<close>[unfolded convex_contains_segment, rule_format, of y y'])
-          (auto simp: dist_commute)
+          (auto simp: dist_commute mem_ball)
       finally have "y + t *\<^sub>R (y' - y) \<in> ?S" .
     } note seg = this
 
     have "\<forall>x\<in>ball y d \<inter> Y. onorm (blinfun_apply (fy x' x) - blinfun_apply (fy x' y)) \<le> e + e"
-      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
+      by (safe intro!: onorm less_imp_le \<open>x' \<in> X\<close> dx) (auto simp: mem_ball dist_commute \<open>0 < d\<close> \<open>y \<in> Y\<close>)
     with seg has_derivative_within_subset[OF assms(2)[OF \<open>x' \<in> X\<close>]]
     show "norm (f x' y' - f x' y - (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
       by (rule differentiable_bound_linearization[where S="?S"])
         (auto intro!: \<open>0 < d\<close> \<open>y \<in> Y\<close>)
   qed
   moreover
-  let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx x y) (x' - x)) \<le> norm (x' - x) * e"
-  from fx[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>, unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
+  let ?le = "\<lambda>x'. norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
+  from fx[unfolded has_derivative_within, THEN conjunct2, THEN tendstoD, OF \<open>0 < e\<close>]
   have "\<forall>\<^sub>F x' in at x within X. ?le x'"
     by eventually_elim
-       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps split: if_split_asm)
+       (auto simp: dist_norm divide_simps blinfun.bilinear_simps field_simps fx.zero split: if_split_asm)
   then have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. ?le x'"
     by (rule eventually_at_Pair_within_TimesI1)
-       (simp add: blinfun.bilinear_simps)
+       (simp add: blinfun.bilinear_simps fx.zero)
   moreover have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y. norm ((x', y') - (x, y)) \<noteq> 0"
     unfolding norm_eq_zero right_minus_eq
     by (auto simp: eventually_at intro!: zero_less_one)
   moreover
-  from fy_cont[unfolded continuous_on_eq_continuous_within, rule_format, OF SigmaI[OF \<open>x \<in> X\<close> \<open>y \<in> Y\<close>],
-      unfolded continuous_within, THEN tendstoD, OF \<open>0 < e\<close>]
+  from fy_cont[THEN tendstoD, OF \<open>0 < e\<close>]
   have "\<forall>\<^sub>F x' in at x within X. norm (fy x' y - fy x y) < e"
     unfolding eventually_at
     using \<open>y \<in> Y\<close>
@@ -3032,22 +3038,22 @@
        (simp add: blinfun.bilinear_simps \<open>0 < e\<close>)
   ultimately
   have "\<forall>\<^sub>F (x', y') in at (x, y) within X \<times> Y.
-            norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R
+            norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R
               norm ((x', y') - (x, y)))
             < e'"
     apply eventually_elim
   proof safe
     fix x' y'
-    have "norm (f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) \<le>
+    have "norm (f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) \<le>
         norm (f x' y' - f x' y - fy x' y (y' - y)) +
         norm (fy x y (y' - y) - fy x' y (y' - y)) +
-        norm (f x' y - f x y - fx x y (x' - x))"
+        norm (f x' y - f x y - fx (x' - x))"
       by norm
     also
     assume nz: "norm ((x', y') - (x, y)) \<noteq> 0"
       and nfy: "norm (fy x' y - fy x y) < e"
     assume "norm (f x' y' - f x' y - blinfun_apply (fy x' y) (y' - y)) \<le> norm (y' - y) * (e + e)"
-    also assume "norm (f x' y - f x y - blinfun_apply (fx x y) (x' - x)) \<le> norm (x' - x) * e"
+    also assume "norm (f x' y - f x y - (fx) (x' - x)) \<le> norm (x' - x) * e"
     also
     have "norm ((fy x y) (y' - y) - (fy x' y) (y' - y)) \<le> norm ((fy x y) - (fy x' y)) * norm (y' - y)"
       by (auto simp: blinfun.bilinear_simps[symmetric] intro!: norm_blinfun)
@@ -3070,11 +3076,80 @@
     also have "\<dots> < norm ((x', y') - (x, y)) * e'"
       using \<open>0 < e'\<close> nz
       by (auto simp: e_def)
-    finally show "norm ((f x' y' - f x y - (fx x y (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
+    finally show "norm ((f x' y' - f x y - (fx (x' - x) + fy x y (y' - y))) /\<^sub>R norm ((x', y') - (x, y))) < e'"
       by (auto simp: divide_simps dist_norm mult.commute)
   qed
   then show ?case
     by eventually_elim (auto simp: dist_norm field_simps)
-qed (auto intro!: bounded_linear_intros simp: split_beta')
+next
+  from has_derivative_bounded_linear[OF fx]
+  obtain fxb where "fx = blinfun_apply fxb"
+    by (metis bounded_linear_Blinfun_apply)
+  then show "bounded_linear (\<lambda>(tx, ty). fx tx + blinfun_apply (fy x y) ty)"
+    by (auto intro!: bounded_linear_intros simp: split_beta')
+qed
+
+
+subsection \<open>Differentiable case distinction\<close>
+
+lemma has_derivative_within_If_eq:
+  "((\<lambda>x. if P x then f x else g x) has_derivative f') (at x within s) =
+    (bounded_linear f' \<and>
+     ((\<lambda>y.(if P y then (f y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)
+           else (g y - ((if P x then f x else g x) + f' (y - x)))/\<^sub>R norm (y - x)))
+      \<longlongrightarrow> 0) (at x within s))"
+  (is "_ = (_ \<and> (?if \<longlongrightarrow> 0) _)")
+proof -
+  have "(\<lambda>y. (1 / norm (y - x)) *\<^sub>R
+           ((if P y then f y else g y) -
+            ((if P x then f x else g x) + f' (y - x)))) = ?if"
+    by (auto simp: inverse_eq_divide)
+  thus ?thesis by (auto simp: has_derivative_within)
+qed
+
+lemma has_derivative_If_within_closures:
+  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (f has_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (g has_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+  assumes x_in: "x \<in> s \<union> t"
+  shows "((\<lambda>x. if x \<in> s then f x else g x) has_derivative
+      (if x \<in> s then f' x else g' x)) (at x within (s \<union> t))"
+proof -
+  from f' x_in interpret f': bounded_linear "if x \<in> s then f' x else (\<lambda>x. 0)"
+    by (auto simp add: has_derivative_within)
+  from g' interpret g': bounded_linear "if x \<in> t then g' x else (\<lambda>x. 0)"
+    by (auto simp add: has_derivative_within)
+  have bl: "bounded_linear (if x \<in> s then f' x else g' x)"
+    using f'.scaleR f'.bounded f'.add g'.scaleR g'.bounded g'.add x_in
+    by (unfold_locales; force)
+  show ?thesis
+    using f' g' closure_subset[of t] closure_subset[of s]
+    unfolding has_derivative_within_If_eq
+    by (intro conjI bl tendsto_If_within_closures x_in)
+      (auto simp: has_derivative_within inverse_eq_divide connect connect' set_mp)
+qed
+
+lemma has_vector_derivative_If_within_closures:
+  assumes x_in: "x \<in> s \<union> t"
+  assumes "u = s \<union> t"
+  assumes f': "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (f has_vector_derivative f' x) (at x within s \<union> (closure s \<inter> closure t))"
+  assumes g': "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+    (g has_vector_derivative g' x) (at x within t \<union> (closure s \<inter> closure t))"
+  assumes connect: "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f x = g x"
+  assumes connect': "x \<in> closure s \<Longrightarrow> x \<in> closure t \<Longrightarrow> f' x = g' x"
+  shows "((\<lambda>x. if x \<in> s then f x else g x) has_vector_derivative
+    (if x \<in> s then f' x else g' x)) (at x within u)"
+  unfolding has_vector_derivative_def assms
+  using x_in
+  apply (intro has_derivative_If_within_closures[where
+        ?f' = "\<lambda>x a. a *\<^sub>R f' x" and ?g' = "\<lambda>x a. a *\<^sub>R g' x",
+        THEN has_derivative_eq_rhs])
+  subgoal by (rule f'[unfolded has_vector_derivative_def]; assumption)
+  subgoal by (rule g'[unfolded has_vector_derivative_def]; assumption)
+  by (auto simp: assms)
 
 end
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Euclidean_Space.thy
--- a/src/HOL/Analysis/Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -84,6 +84,10 @@
 lemma (in euclidean_space) euclidean_representation: "(\<Sum>b\<in>Basis. inner x b *\<^sub>R b) = x"
   unfolding euclidean_representation_sum by simp
 
+lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (inner x b) * (inner y b))"
+  by (subst (1 2) euclidean_representation [symmetric])
+    (simp add: inner_sum_right inner_Basis ac_simps)
+
 lemma (in euclidean_space) choice_Basis_iff:
   fixes P :: "'a \<Rightarrow> real \<Rightarrow> bool"
   shows "(\<forall>i\<in>Basis. \<exists>x. P i x) \<longleftrightarrow> (\<exists>x. \<forall>i\<in>Basis. P i (inner x i))"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Finite_Cartesian_Product.thy
--- a/src/HOL/Analysis/Finite_Cartesian_Product.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Finite_Cartesian_Product.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -20,9 +20,19 @@
 
 declare vec_lambda_inject [simplified, simp]
 
+bundle vec_syntax begin
 notation
   vec_nth (infixl "$" 90) and
   vec_lambda (binder "\<chi>" 10)
+end
+
+bundle no_vec_syntax begin
+no_notation
+  vec_nth (infixl "$" 90) and
+  vec_lambda (binder "\<chi>" 10)
+end
+
+unbundle vec_syntax
 
 (*
   Translate "'b ^ 'n" into "'b ^ ('n :: finite)". When 'n has already more than
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -621,6 +621,11 @@
   with False show ?thesis by (simp add: not_integrable_integral)
 qed
 
+lemma integral_mult:
+  fixes K::real
+  shows "f integrable_on X \<Longrightarrow> K * integral X f = integral X (\<lambda>x. K * f x)"
+  unfolding real_scaleR_def[symmetric] integral_cmul ..
+
 lemma integral_neg [simp]: "integral S (\<lambda>x. - f x) = - integral S f"
 proof (cases "f integrable_on S")
   case True then show ?thesis
@@ -2549,6 +2554,13 @@
 
 lemmas integrable_continuous_real = integrable_continuous_interval[where 'b=real]
 
+lemma integrable_continuous_closed_segment:
+  fixes f :: "real \<Rightarrow> 'a::banach"
+  assumes "continuous_on (closed_segment a b) f"
+  shows "f integrable_on (closed_segment a b)"
+  using assms
+  by (auto intro!: integrable_continuous_interval simp: closed_segment_eq_real_ivl)
+
 
 subsection \<open>Specialization of additivity to one dimension.\<close>
 
@@ -2722,6 +2734,32 @@
 
 subsection \<open>Taylor series expansion\<close>
 
+lemma mvt_integral:
+  fixes f::"'a::real_normed_vector\<Rightarrow>'b::banach"
+  assumes f'[derivative_intros]:
+    "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
+  assumes line_in: "\<And>t. t \<in> {0..1} \<Longrightarrow> x + t *\<^sub>R y \<in> S"
+  shows "f (x + y) - f x = integral {0..1} (\<lambda>t. f' (x + t *\<^sub>R y) y)" (is ?th1)
+proof -
+  from assms have subset: "(\<lambda>xa. x + xa *\<^sub>R y) ` {0..1} \<subseteq> S" by auto
+  note [derivative_intros] =
+    has_derivative_subset[OF _ subset]
+    has_derivative_in_compose[where f="(\<lambda>xa. x + xa *\<^sub>R y)" and g = f]
+  note [continuous_intros] =
+    continuous_on_compose2[where f="(\<lambda>xa. x + xa *\<^sub>R y)"]
+    continuous_on_subset[OF _ subset]
+  have "\<And>t. t \<in> {0..1} \<Longrightarrow>
+    ((\<lambda>t. f (x + t *\<^sub>R y)) has_vector_derivative f' (x + t *\<^sub>R y) y)
+    (at t within {0..1})"
+    using assms
+    by (auto simp: has_vector_derivative_def
+        linear_cmul[OF has_derivative_linear[OF f'], symmetric]
+      intro!: derivative_eq_intros)
+  from fundamental_theorem_of_calculus[rule_format, OF _ this]
+  show ?th1
+    by (auto intro!: integral_unique[symmetric])
+qed
+
 lemma (in bounded_bilinear) sum_prod_derivatives_has_vector_derivative:
   assumes "p>0"
   and f0: "Df 0 = f"
@@ -2835,7 +2873,6 @@
 qed
 
 
-
 subsection \<open>Only need trivial subintervals if the interval itself is trivial.\<close>
 
 proposition division_of_nontrivial:
@@ -3024,6 +3061,21 @@
   unfolding integrable_on_def
   by (auto intro!: has_integral_combine)
 
+lemma integral_minus_sets:
+  fixes f::"real \<Rightarrow> 'a::banach"
+  shows "c \<le> a \<Longrightarrow> c \<le> b \<Longrightarrow> f integrable_on {c .. max a b} \<Longrightarrow>
+    integral {c .. a} f - integral {c .. b} f =
+    (if a \<le> b then - integral {a .. b} f else integral {b .. a} f)"
+  using integral_combine[of c a b f]  integral_combine[of c b a f]
+  by (auto simp: algebra_simps max_def)
+
+lemma integral_minus_sets':
+  fixes f::"real \<Rightarrow> 'a::banach"
+  shows "c \<ge> a \<Longrightarrow> c \<ge> b \<Longrightarrow> f integrable_on {min a b .. c} \<Longrightarrow>
+    integral {a .. c} f - integral {b .. c} f =
+    (if a \<le> b then integral {a .. b} f else - integral {b .. a} f)"
+  using integral_combine[of b a c f] integral_combine[of a b c f]
+  by (auto simp: algebra_simps min_def)
 
 subsection \<open>Reduce integrability to "local" integrability.\<close>
 
@@ -3129,13 +3181,19 @@
 using assms integral_has_vector_derivative_continuous_at [OF integrable_continuous_real]
   by (fastforce simp: continuous_on_eq_continuous_within)
 
+lemma integral_has_real_derivative:
+  assumes "continuous_on {a..b} g"
+  assumes "t \<in> {a..b}"
+  shows "((\<lambda>x. integral {a..x} g) has_real_derivative g t) (at t within {a..b})"
+  using integral_has_vector_derivative[of a b g t] assms
+  by (auto simp: has_field_derivative_iff_has_vector_derivative)
+
 lemma antiderivative_continuous:
   fixes q b :: real
   assumes "continuous_on {a..b} f"
   obtains g where "\<And>x. x \<in> {a..b} \<Longrightarrow> (g has_vector_derivative (f x::_::banach)) (at x within {a..b})"
   using integral_has_vector_derivative[OF assms] by auto
 
-
 subsection \<open>Combined fundamental theorem of calculus.\<close>
 
 lemma antiderivative_integral_continuous:
@@ -3149,7 +3207,8 @@
   have "(f has_integral g v - g u) {u..v}" if "u \<in> {a..b}" "v \<in> {a..b}" "u \<le> v" for u v
   proof -
     have "\<And>x. x \<in> cbox u v \<Longrightarrow> (g has_vector_derivative f x) (at x within cbox u v)"
-      by (meson g has_vector_derivative_within_subset interval_subset_is_interval is_interval_closed_interval subsetCE that(1) that(2))
+      by (metis atLeastAtMost_iff atLeastatMost_subset_iff box_real(2) g
+          has_vector_derivative_within_subset subsetCE that(1,2))
     then show ?thesis
       by (metis box_real(2) that(3) fundamental_theorem_of_calculus)
   qed
@@ -4125,6 +4184,28 @@
     by (rule continuous_on_eq) (auto intro!: continuous_intros indefinite_integral_continuous_1 assms)
 qed
 
+theorem integral_has_vector_derivative':
+  fixes f :: "real \<Rightarrow> 'b::banach"
+  assumes "continuous_on {a..b} f"
+    and "x \<in> {a..b}"
+  shows "((\<lambda>u. integral {u..b} f) has_vector_derivative - f x) (at x within {a..b})"
+proof -
+  have *: "integral {x..b} f = integral {a .. b} f - integral {a .. x} f" if "a \<le> x" "x \<le> b" for x
+    using integral_combine[of a x b for x, OF that integrable_continuous_real[OF assms(1)]]
+    by (simp add: algebra_simps)
+  show ?thesis
+    using \<open>x \<in> _\<close> *
+    by (rule has_vector_derivative_transform)
+      (auto intro!: derivative_eq_intros assms integral_has_vector_derivative)
+qed
+
+lemma integral_has_real_derivative':
+  assumes "continuous_on {a..b} g"
+  assumes "t \<in> {a..b}"
+  shows "((\<lambda>x. integral {x..b} g) has_real_derivative -g t) (at t within {a..b})"
+  using integral_has_vector_derivative'[OF assms]
+  by (auto simp: has_field_derivative_iff_has_vector_derivative)
+
 
 subsection \<open>This doesn't directly involve integration, but that gives an easy proof.\<close>
 
@@ -4661,6 +4742,10 @@
   shows "f integrable_on S \<longleftrightarrow> f integrable_on T"
   by (blast intro: integrable_spike_set assms negligible_subset)
 
+lemma integrable_on_insert_iff: "f integrable_on (insert x X) \<longleftrightarrow> f integrable_on X"
+  for f::"_ \<Rightarrow> 'a::banach"
+  by (rule integrable_spike_set_eq) (auto simp: insert_Diff_if)
+
 lemma has_integral_interior:
   fixes f :: "'a :: euclidean_space \<Rightarrow> 'b :: banach"
   shows "negligible(frontier S) \<Longrightarrow> (f has_integral y) (interior S) \<longleftrightarrow> (f has_integral y) S"
@@ -6049,6 +6134,26 @@
   qed
 qed
 
+lemma continuous_on_imp_absolutely_integrable_on:
+  fixes f::"real \<Rightarrow> 'a::banach"
+  shows "continuous_on {a..b} f \<Longrightarrow>
+    norm (integral {a..b} f) \<le> integral {a..b} (\<lambda>x. norm (f x))"
+  by (intro integral_norm_bound_integral integrable_continuous_real continuous_on_norm) auto
+
+lemma integral_bound:
+  fixes f::"real \<Rightarrow> 'a::banach"
+  assumes "a \<le> b"
+  assumes "continuous_on {a .. b} f"
+  assumes "\<And>t. t \<in> {a .. b} \<Longrightarrow> norm (f t) \<le> B"
+  shows "norm (integral {a .. b} f) \<le> B * (b - a)"
+proof -
+  note continuous_on_imp_absolutely_integrable_on[OF assms(2)]
+  also have "integral {a..b} (\<lambda>x. norm (f x)) \<le> integral {a..b} (\<lambda>_. B)"
+    by (rule integral_le)
+      (auto intro!: integrable_continuous_real continuous_intros assms)
+  also have "\<dots> = B * (b - a)" using assms by simp
+  finally show ?thesis .
+qed
 
 lemma integral_norm_bound_integral_component:
   fixes f :: "'n::euclidean_space \<Rightarrow> 'a::banach"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/L2_Norm.thy
--- a/src/HOL/Analysis/L2_Norm.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/L2_Norm.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -98,13 +98,6 @@
   qed
 qed
 
-lemma sqrt_sum_squares_le_sum:
-  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
-  apply (rule power2_le_imp_le)
-  apply (simp add: power2_sum)
-  apply simp
-  done
-
 lemma L2_set_le_sum [rule_format]:
   "(\<forall>i\<in>A. 0 \<le> f i) \<longrightarrow> L2_set f A \<le> sum f A"
   apply (cases "finite A")
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Linear_Algebra.thy
--- a/src/HOL/Analysis/Linear_Algebra.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Linear_Algebra.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -2987,10 +2987,6 @@
 lemma infnorm_le_norm: "infnorm x \<le> norm x"
   by (simp add: Basis_le_norm infnorm_Max)
 
-lemma (in euclidean_space) euclidean_inner: "inner x y = (\<Sum>b\<in>Basis. (x \<bullet> b) * (y \<bullet> b))"
-  by (subst (1 2) euclidean_representation [symmetric])
-    (simp add: inner_sum_right inner_Basis ac_simps)
-
 lemma norm_le_infnorm:
   fixes x :: "'a::euclidean_space"
   shows "norm x \<le> sqrt DIM('a) * infnorm x"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Operator_Norm.thy
--- a/src/HOL/Analysis/Operator_Norm.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Operator_Norm.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -235,4 +235,13 @@
   shows "onorm (\<lambda>x. f x + g x) < e"
   using assms by (rule onorm_triangle [THEN order_le_less_trans])
 
+lemma onorm_sum:
+  assumes "finite S"
+  assumes "\<And>s. s \<in> S \<Longrightarrow> bounded_linear (f s)"
+  shows "onorm (\<lambda>x. sum (\<lambda>s. f s x) S) \<le> sum (\<lambda>s. onorm (f s)) S"
+  using assms
+  by (induction) (auto simp: onorm_zero intro!: onorm_triangle_le bounded_linear_sum)
+
+lemmas onorm_sum_le = onorm_sum[THEN order_trans]
+
 end
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Ordered_Euclidean_Space.thy
--- a/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Ordered_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -214,9 +214,20 @@
   using image_smult_cbox[of m a b]
   by (simp add: cbox_interval)
 
-lemma is_interval_closed_interval [simp]:
-  "is_interval {a .. (b::'a::ordered_euclidean_space)}"
-  by (metis cbox_interval is_interval_cbox)
+lemma [simp]:
+  fixes a b::"'a::ordered_euclidean_space" and r s::real
+  shows is_interval_io: "is_interval {..<r}"
+    and is_interval_ic: "is_interval {..a}"
+    and is_interval_oi: "is_interval {r<..}"
+    and is_interval_ci: "is_interval {a..}"
+    and is_interval_oo: "is_interval {r<..<s}"
+    and is_interval_oc: "is_interval {r<..s}"
+    and is_interval_co: "is_interval {r..<s}"
+    and is_interval_cc: "is_interval {b..a}"
+  by (force simp: is_interval_def eucl_le[where 'a='a])+
+
+lemma is_interval_real_ereal_oo: "is_interval (real_of_ereal ` {N<..<M::ereal})"
+  by (auto simp: real_atLeastGreaterThan_eq)
 
 lemma compact_interval [simp]:
   fixes a b::"'a::ordered_euclidean_space"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Product_Vector.thy
--- a/src/HOL/Analysis/Product_Vector.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Product_Vector.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -306,6 +306,11 @@
     by (simp add: norm_Pair divide_right_mono order_trans [OF sqrt_add_le_add_sqrt])
 qed simp
 
+lemma differentiable_Pair [simp, derivative_intros]:
+  "f differentiable at x within s \<Longrightarrow> g differentiable at x within s \<Longrightarrow>
+    (\<lambda>x. (f x, g x)) differentiable at x within s"
+  unfolding differentiable_def by (blast intro: has_derivative_Pair)
+
 lemmas has_derivative_fst [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_fst]
 lemmas has_derivative_snd [derivative_intros] = bounded_linear.has_derivative [OF bounded_linear_snd]
 
@@ -313,6 +318,17 @@
   "((\<lambda>p. f (fst p) (snd p)) has_derivative f') F \<Longrightarrow> ((\<lambda>(a, b). f a b) has_derivative f') F"
   unfolding split_beta' .
 
+
+subsubsection \<open>Vector derivatives involving pairs\<close>
+
+lemma has_vector_derivative_Pair[derivative_intros]:
+  assumes "(f has_vector_derivative f') (at x within s)"
+    "(g has_vector_derivative g') (at x within s)"
+  shows "((\<lambda>x. (f x, g x)) has_vector_derivative (f', g')) (at x within s)"
+  using assms
+  by (auto simp: has_vector_derivative_def intro!: derivative_eq_intros)
+
+
 subsection \<open>Product is an inner product space\<close>
 
 instantiation prod :: (real_inner, real_inner) real_inner
@@ -368,4 +384,9 @@
 lemma norm_snd_le: "norm y \<le> norm (x,y)"
   by (metis dist_snd_le snd_conv snd_zero norm_conv_dist)
 
+lemma norm_Pair_le:
+  shows "norm (x, y) \<le> norm x + norm y"
+  unfolding norm_Pair
+  by (metis norm_ge_zero sqrt_sum_squares_le_sum)
+
 end
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Riemann_Mapping.thy
--- a/src/HOL/Analysis/Riemann_Mapping.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Riemann_Mapping.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -489,7 +489,7 @@
     let ?g = "\<lambda>z. (SOME g. polynomial_function g \<and> path_image g \<subseteq> S \<and> pathstart g = a \<and> pathfinish g = z)"
     show "((\<lambda>z. contour_integral (?g z) f) has_field_derivative f x)
           (at x)"
-    proof (simp add: has_field_derivative_def has_derivative_at bounded_linear_mult_right, rule Lim_transform)
+    proof (simp add: has_field_derivative_def has_derivative_at2 bounded_linear_mult_right, rule Lim_transform)
       show "(\<lambda>y. inverse(norm(y - x)) *\<^sub>R (contour_integral(linepath x y) f - f x * (y - x))) \<midarrow>x\<rightarrow> 0"
       proof (clarsimp simp add: Lim_at)
         fix e::real assume "e > 0"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Starlike.thy
--- a/src/HOL/Analysis/Starlike.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Starlike.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -13,9 +13,87 @@
 
 begin
 
+subsection \<open>Midpoint\<close>
+
 definition midpoint :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a"
   where "midpoint a b = (inverse (2::real)) *\<^sub>R (a + b)"
 
+lemma midpoint_idem [simp]: "midpoint x x = x"
+  unfolding midpoint_def
+  unfolding scaleR_right_distrib
+  unfolding scaleR_left_distrib[symmetric]
+  by auto
+
+lemma midpoint_sym: "midpoint a b = midpoint b a"
+  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
+
+lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
+proof -
+  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
+    by simp
+  then show ?thesis
+    unfolding midpoint_def scaleR_2 [symmetric] by simp
+qed
+
+lemma
+  fixes a::real
+  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
+                    and le_midpoint_1: "midpoint a b \<le> b"
+  by (simp_all add: midpoint_def assms)
+
+lemma dist_midpoint:
+  fixes a b :: "'a::real_normed_vector" shows
+  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
+  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
+  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
+  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
+proof -
+  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
+    unfolding equation_minus_iff by auto
+  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
+    by auto
+  note scaleR_right_distrib [simp]
+  show ?t1
+    unfolding midpoint_def dist_norm
+    apply (rule **)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+  show ?t2
+    unfolding midpoint_def dist_norm
+    apply (rule *)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+  show ?t3
+    unfolding midpoint_def dist_norm
+    apply (rule *)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+  show ?t4
+    unfolding midpoint_def dist_norm
+    apply (rule **)
+    apply (simp add: scaleR_right_diff_distrib)
+    apply (simp add: scaleR_2)
+    done
+qed
+
+lemma midpoint_eq_endpoint [simp]:
+  "midpoint a b = a \<longleftrightarrow> a = b"
+  "midpoint a b = b \<longleftrightarrow> a = b"
+  unfolding midpoint_eq_iff by auto
+
+lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
+  using midpoint_eq_iff by metis
+
+lemma midpoint_linear_image:
+   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
+by (simp add: linear_iff midpoint_def)
+
+
+subsection \<open>Line segments\<close>
+
 definition closed_segment :: "'a::real_vector \<Rightarrow> 'a \<Rightarrow> 'a set"
   where "closed_segment a b = {(1 - u) *\<^sub>R a + u *\<^sub>R b | u::real. 0 \<le> u \<and> u \<le> 1}"
 
@@ -106,86 +184,6 @@
   apply (auto simp: in_segment scaleR_conv_of_real elim!: ex_forward del: exE)
   using of_real_eq_iff by fastforce
 
-lemma midpoint_idem [simp]: "midpoint x x = x"
-  unfolding midpoint_def
-  unfolding scaleR_right_distrib
-  unfolding scaleR_left_distrib[symmetric]
-  by auto
-
-lemma midpoint_sym: "midpoint a b = midpoint b a"
-  unfolding midpoint_def by (auto simp add: scaleR_right_distrib)
-
-lemma midpoint_eq_iff: "midpoint a b = c \<longleftrightarrow> a + b = c + c"
-proof -
-  have "midpoint a b = c \<longleftrightarrow> scaleR 2 (midpoint a b) = scaleR 2 c"
-    by simp
-  then show ?thesis
-    unfolding midpoint_def scaleR_2 [symmetric] by simp
-qed
-
-lemma
-  fixes a::real
-  assumes "a \<le> b" shows ge_midpoint_1: "a \<le> midpoint a b"
-                    and le_midpoint_1: "midpoint a b \<le> b"
-  by (simp_all add: midpoint_def assms)
-
-lemma dist_midpoint:
-  fixes a b :: "'a::real_normed_vector" shows
-  "dist a (midpoint a b) = (dist a b) / 2" (is ?t1)
-  "dist b (midpoint a b) = (dist a b) / 2" (is ?t2)
-  "dist (midpoint a b) a = (dist a b) / 2" (is ?t3)
-  "dist (midpoint a b) b = (dist a b) / 2" (is ?t4)
-proof -
-  have *: "\<And>x y::'a. 2 *\<^sub>R x = - y \<Longrightarrow> norm x = (norm y) / 2"
-    unfolding equation_minus_iff by auto
-  have **: "\<And>x y::'a. 2 *\<^sub>R x =   y \<Longrightarrow> norm x = (norm y) / 2"
-    by auto
-  note scaleR_right_distrib [simp]
-  show ?t1
-    unfolding midpoint_def dist_norm
-    apply (rule **)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-  show ?t2
-    unfolding midpoint_def dist_norm
-    apply (rule *)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-  show ?t3
-    unfolding midpoint_def dist_norm
-    apply (rule *)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-  show ?t4
-    unfolding midpoint_def dist_norm
-    apply (rule **)
-    apply (simp add: scaleR_right_diff_distrib)
-    apply (simp add: scaleR_2)
-    done
-qed
-
-lemma midpoint_eq_endpoint [simp]:
-  "midpoint a b = a \<longleftrightarrow> a = b"
-  "midpoint a b = b \<longleftrightarrow> a = b"
-  unfolding midpoint_eq_iff by auto
-
-lemma midpoint_plus_self [simp]: "midpoint a b + midpoint a b = a + b"
-  using midpoint_eq_iff by metis
-
-lemma midpoint_linear_image:
-   "linear f \<Longrightarrow> midpoint(f a)(f b) = f(midpoint a b)"
-by (simp add: linear_iff midpoint_def)
-
-subsection\<open>Starlike sets\<close>
-
-definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
-
-lemma starlike_UNIV [simp]: "starlike UNIV"
-  by (simp add: starlike_def)
-
 lemma convex_contains_segment:
   "convex S \<longleftrightarrow> (\<forall>a\<in>S. \<forall>b\<in>S. closed_segment a b \<subseteq> S)"
   unfolding convex_alt closed_segment_def by auto
@@ -197,10 +195,6 @@
     "\<lbrakk>x \<in> convex hull S; y \<in> convex hull S\<rbrakk> \<Longrightarrow> closed_segment x y \<subseteq> convex hull S"
   using convex_contains_segment by blast
 
-lemma convex_imp_starlike:
-  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
-  unfolding convex_contains_segment starlike_def by auto
-
 lemma segment_convex_hull:
   "closed_segment a b = convex hull {a,b}"
 proof -
@@ -349,7 +343,7 @@
   proof -
     have "norm ((1 - 1 * u) *\<^sub>R (a - b)) = (1 - 1 * u) * norm (a - b)"
       using \<open>u \<le> 1\<close> by force
-    then show ?thesis                     
+    then show ?thesis
       by (simp add: dist_norm real_vector.scale_right_diff_distrib)
   qed
   also have "... \<le> dist a b"
@@ -581,7 +575,6 @@
     by (metis image_comp convex_translation)
 qed
 
-
 lemmas convex_segment = convex_closed_segment convex_open_segment
 
 lemma connected_segment [iff]:
@@ -589,6 +582,33 @@
   shows "connected (closed_segment x y)"
   by (simp add: convex_connected)
 
+lemma is_interval_closed_segment_1[intro, simp]: "is_interval (closed_segment a b)" for a b::real
+  by (auto simp: is_interval_convex_1)
+
+lemma IVT'_closed_segment_real:
+  fixes f :: "real \<Rightarrow> real"
+  assumes "y \<in> closed_segment (f a) (f b)"
+  assumes "continuous_on (closed_segment a b) f"
+  shows "\<exists>x \<in> closed_segment a b. f x = y"
+  using IVT'[of f a y b]
+    IVT'[of "-f" a "-y" b]
+    IVT'[of f b y a]
+    IVT'[of "-f" b "-y" a] assms
+  by (cases "a \<le> b"; cases "f b \<ge> f a") (auto simp: closed_segment_eq_real_ivl continuous_on_minus)
+
+
+subsection\<open>Starlike sets\<close>
+
+definition "starlike S \<longleftrightarrow> (\<exists>a\<in>S. \<forall>x\<in>S. closed_segment a x \<subseteq> S)"
+
+lemma starlike_UNIV [simp]: "starlike UNIV"
+  by (simp add: starlike_def)
+
+lemma convex_imp_starlike:
+  "convex S \<Longrightarrow> S \<noteq> {} \<Longrightarrow> starlike S"
+  unfolding convex_contains_segment starlike_def by auto
+
+
 lemma affine_hull_closed_segment [simp]:
      "affine hull (closed_segment a b) = affine hull {a,b}"
   by (simp add: segment_convex_hull)
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -7,7 +7,7 @@
 section \<open>Elementary topology in Euclidean space.\<close>
 
 theory Topology_Euclidean_Space
-imports                                                         
+imports
   "HOL-Library.Indicator_Function"
   "HOL-Library.Countable_Set"
   "HOL-Library.FuncSet"
@@ -1112,6 +1112,9 @@
 lemma ball_subset_cball [simp, intro]: "ball x e \<subseteq> cball x e"
   by (simp add: subset_eq)
 
+lemma mem_ball_imp_mem_cball: "x \<in> ball y e \<Longrightarrow> x \<in> cball y e"
+  by (auto simp: mem_ball mem_cball)
+
 lemma sphere_cball [simp,intro]: "sphere z r \<subseteq> cball z r"
   by force
 
@@ -1124,6 +1127,22 @@
 lemma subset_cball[intro]: "d \<le> e \<Longrightarrow> cball x d \<subseteq> cball x e"
   by (simp add: subset_eq)
 
+lemma mem_ball_leI: "x \<in> ball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> ball y f"
+  by (auto simp: mem_ball mem_cball)
+
+lemma mem_cball_leI: "x \<in> cball y e \<Longrightarrow> e \<le> f \<Longrightarrow> x \<in> cball y f"
+  by (auto simp: mem_ball mem_cball)
+
+lemma cball_trans: "y \<in> cball z b \<Longrightarrow> x \<in> cball y a \<Longrightarrow> x \<in> cball z (b + a)"
+  unfolding mem_cball
+proof -
+  have "dist z x \<le> dist z y + dist y x"
+    by (rule dist_triangle)
+  also assume "dist z y \<le> b"
+  also assume "dist y x \<le> a"
+  finally show "dist z x \<le> b + a" by arith
+qed
+
 lemma ball_max_Un: "ball a (max r s) = ball a r \<union> ball a s"
   by (simp add: set_eq_iff) arith
 
@@ -1253,6 +1272,17 @@
   unfolding dist_norm norm_eq_sqrt_inner L2_set_def
   by (subst euclidean_inner) (simp add: power2_eq_square inner_diff_left)
 
+lemma norm_nth_le: "norm (x \<bullet> i) \<le> norm x" if "i \<in> Basis"
+proof -
+  have "(x \<bullet> i)\<^sup>2 = (\<Sum>i\<in>{i}. (x \<bullet> i)\<^sup>2)"
+    by simp
+  also have "\<dots> \<le> (\<Sum>i\<in>Basis. (x \<bullet> i)\<^sup>2)"
+    by (intro sum_mono2) (auto simp: that)
+  finally show ?thesis
+    unfolding norm_conv_dist euclidean_dist_l2[of x] L2_set_def
+    by (auto intro!: real_le_rsqrt)
+qed
+
 lemma eventually_nhds_ball: "d > 0 \<Longrightarrow> eventually (\<lambda>x. x \<in> ball z d) (nhds z)"
   by (rule eventually_nhds_in_open) simp_all
 
@@ -1262,6 +1292,20 @@
 lemma eventually_at_ball': "d > 0 \<Longrightarrow> eventually (\<lambda>t. t \<in> ball z d \<and> t \<noteq> z \<and> t \<in> A) (at z within A)"
   unfolding eventually_at by (intro exI[of _ d]) (simp_all add: dist_commute)
 
+lemma at_within_ball: "e > 0 \<Longrightarrow> dist x y < e \<Longrightarrow> at y within ball x e = at y"
+  by (subst at_within_open) auto
+
+lemma atLeastAtMost_eq_cball:
+  fixes a b::real
+  shows "{a .. b} = cball ((a + b)/2) ((b - a)/2)"
+  by (auto simp: dist_real_def field_simps mem_cball)
+
+lemma greaterThanLessThan_eq_ball:
+  fixes a b::real
+  shows "{a <..< b} = ball ((a + b)/2) ((b - a)/2)"
+  by (auto simp: dist_real_def field_simps mem_ball)
+
+
 subsection \<open>Boxes\<close>
 
 abbreviation One :: "'a::euclidean_space"
@@ -1834,6 +1878,14 @@
 definition "is_interval (s::('a::euclidean_space) set) \<longleftrightarrow>
   (\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i\<in>Basis. ((a\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> b\<bullet>i) \<or> (b\<bullet>i \<le> x\<bullet>i \<and> x\<bullet>i \<le> a\<bullet>i))) \<longrightarrow> x \<in> s)"
 
+lemma is_interval_1:
+  "is_interval (s::real set) \<longleftrightarrow> (\<forall>a\<in>s. \<forall>b\<in>s. \<forall> x. a \<le> x \<and> x \<le> b \<longrightarrow> x \<in> s)"
+  unfolding is_interval_def by auto
+
+lemma is_interval_inter: "is_interval X \<Longrightarrow> is_interval Y \<Longrightarrow> is_interval (X \<inter> Y)"
+  unfolding is_interval_def
+  by blast
+
 lemma is_interval_cbox [simp]: "is_interval (cbox a (b::'a::euclidean_space))" (is ?th1)
   and is_interval_box [simp]: "is_interval (box a b)" (is ?th2)
   unfolding is_interval_def mem_box Ball_def atLeastAtMost_iff
@@ -1916,6 +1968,88 @@
     by blast
 qed
 
+lemma is_real_interval_union:
+  "is_interval (X \<union> Y)"
+  if X: "is_interval X" and Y: "is_interval Y" and I: "(X \<noteq> {} \<Longrightarrow> Y \<noteq> {} \<Longrightarrow> X \<inter> Y \<noteq> {})"
+  for X Y::"real set"
+proof -
+  consider "X \<noteq> {}" "Y \<noteq> {}" | "X = {}" | "Y = {}" by blast
+  then show ?thesis
+  proof cases
+    case 1
+    then obtain r where "r \<in> X \<or> X \<inter> Y = {}" "r \<in> Y \<or> X \<inter> Y = {}"
+      by blast
+    then show ?thesis
+      using I 1 X Y unfolding is_interval_1
+      by (metis (full_types) Un_iff le_cases)
+  qed (use that in auto)
+qed
+
+lemma is_interval_translationI:
+  assumes "is_interval X"
+  shows "is_interval ((+) x ` X)"
+  unfolding is_interval_def
+proof safe
+  fix b d e
+  assume "b \<in> X" "d \<in> X"
+    "\<forall>i\<in>Basis. (x + b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + d) \<bullet> i \<or>
+       (x + d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (x + b) \<bullet> i"
+  hence "e - x \<in> X"
+    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "e - x"])
+      (auto simp: algebra_simps)
+  thus "e \<in> (+) x ` X" by force
+qed
+
+lemma is_interval_uminusI:
+  assumes "is_interval X"
+  shows "is_interval (uminus ` X)"
+  unfolding is_interval_def
+proof safe
+  fix b d e
+  assume "b \<in> X" "d \<in> X"
+    "\<forall>i\<in>Basis. (- b) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- d) \<bullet> i \<or>
+       (- d) \<bullet> i \<le> e \<bullet> i \<and> e \<bullet> i \<le> (- b) \<bullet> i"
+  hence "- e \<in> X"
+    by (intro mem_is_intervalI[OF assms \<open>b \<in> X\<close> \<open>d \<in> X\<close>, of "- e"])
+      (auto simp: algebra_simps)
+  thus "e \<in> uminus ` X" by force
+qed
+
+lemma is_interval_uminus[simp]: "is_interval (uminus ` x) = is_interval x"
+  using is_interval_uminusI[of x] is_interval_uminusI[of "uminus ` x"]
+  by (auto simp: image_image)
+
+lemma is_interval_neg_translationI:
+  assumes "is_interval X"
+  shows "is_interval ((-) x ` X)"
+proof -
+  have "(-) x ` X = (+) x ` uminus ` X"
+    by (force simp: algebra_simps)
+  also have "is_interval \<dots>"
+    by (metis is_interval_uminusI is_interval_translationI assms)
+  finally show ?thesis .
+qed
+
+lemma is_interval_translation[simp]:
+  "is_interval ((+) x ` X) = is_interval X"
+  using is_interval_neg_translationI[of "(+) x ` X" x]
+  by (auto intro!: is_interval_translationI simp: image_image)
+
+lemma is_interval_minus_translation[simp]:
+  shows "is_interval ((-) x ` X) = is_interval X"
+proof -
+  have "(-) x ` X = (+) x ` uminus ` X"
+    by (force simp: algebra_simps)
+  also have "is_interval \<dots> = is_interval X"
+    by simp
+  finally show ?thesis .
+qed
+
+lemma is_interval_minus_translation'[simp]:
+  shows "is_interval ((\<lambda>x. x - c) ` X) = is_interval X"
+  using is_interval_translation[of "-c" X]
+  by (metis image_cong uminus_add_conv_diff)
+
 
 subsection \<open>Limit points\<close>
 
@@ -2629,6 +2763,15 @@
 lemma not_trivial_limit_within: "\<not> trivial_limit (at x within S) = (x \<in> closure (S - {x}))"
   using islimpt_in_closure by (metis trivial_limit_within)
 
+lemma not_in_closure_trivial_limitI:
+  "x \<notin> closure s \<Longrightarrow> trivial_limit (at x within s)"
+  using not_trivial_limit_within[of x s]
+  by safe (metis Diff_empty Diff_insert0 closure_subset contra_subsetD)
+
+lemma filterlim_at_within_closure_implies_filterlim: "filterlim f l (at x within s)"
+  if "x \<in> closure s \<Longrightarrow> filterlim f l (at x within s)"
+  by (metis bot.extremum filterlim_filtercomap filterlim_mono not_in_closure_trivial_limitI that)
+
 lemma at_within_eq_bot_iff: "at c within A = bot \<longleftrightarrow> c \<notin> closure (A - {c})"
   using not_trivial_limit_within[of c A] by blast
 
@@ -3229,6 +3372,28 @@
   qed
 qed
 
+lemma tendsto_If_within_closures:
+  assumes f: "x \<in> s \<union> (closure s \<inter> closure t) \<Longrightarrow>
+      (f \<longlongrightarrow> l x) (at x within s \<union> (closure s \<inter> closure t))"
+  assumes g: "x \<in> t \<union> (closure s \<inter> closure t) \<Longrightarrow>
+      (g \<longlongrightarrow> l x) (at x within t \<union> (closure s \<inter> closure t))"
+  assumes "x \<in> s \<union> t"
+  shows "((\<lambda>x. if x \<in> s then f x else g x) \<longlongrightarrow> l x) (at x within s \<union> t)"
+proof -
+  have *: "(s \<union> t) \<inter> {x. x \<in> s} = s" "(s \<union> t) \<inter> {x. x \<notin> s} = t - s"
+    by auto
+  have "(f \<longlongrightarrow> l x) (at x within s)"
+    by (rule filterlim_at_within_closure_implies_filterlim)
+       (use \<open>x \<in> _\<close> in \<open>auto simp: inf_commute closure_def intro: tendsto_within_subset[OF f]\<close>)
+  moreover
+  have "(g \<longlongrightarrow> l x) (at x within t - s)"
+    by (rule filterlim_at_within_closure_implies_filterlim)
+      (use \<open>x \<in> _\<close> in
+        \<open>auto intro!: tendsto_within_subset[OF g] simp: closure_def intro: islimpt_subset\<close>)
+  ultimately show ?thesis
+    by (intro filterlim_at_within_If) (simp_all only: *)
+qed
+
 
 subsection \<open>Boundedness\<close>
 
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Analysis/Uniform_Limit.thy
--- a/src/HOL/Analysis/Uniform_Limit.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Analysis/Uniform_Limit.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -438,6 +438,7 @@
   bounded_linear.uniform_limit[OF bounded_linear_mult_right]
   bounded_linear.uniform_limit[OF bounded_linear_scaleR_left]
 
+
 lemmas uniform_limit_uminus[uniform_limit_intros] =
   bounded_linear.uniform_limit[OF bounded_linear_minus[OF bounded_linear_ident]]
 
@@ -728,5 +729,7 @@
 apply (rule continuous_on_cong [THEN iffD1, OF refl _ powser_continuous_suminf [OF r]])
 using sm sums_unique by fastforce
 
+lemmas uniform_limit_subset_union = uniform_limit_on_subset[OF uniform_limit_on_Union]
+
 end
 
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Deriv.thy
--- a/src/HOL/Deriv.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Deriv.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -26,6 +26,13 @@
   most cases @{term s} is either a variable or @{term UNIV}.
 \<close>
 
+text \<open>These are the only cases we'll care about, probably.\<close>
+
+lemma has_derivative_within: "(f has_derivative f') (at x within s) \<longleftrightarrow>
+    bounded_linear f' \<and> ((\<lambda>y. (1 / norm(y - x)) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x within s)"
+  unfolding has_derivative_def tendsto_iff
+  by (subst eventually_Lim_ident_at) (auto simp add: field_simps)
+
 lemma has_derivative_eq_rhs: "(f has_derivative f') F \<Longrightarrow> f' = g' \<Longrightarrow> (f has_derivative g') F"
   by simp
 
@@ -189,6 +196,52 @@
 
 lemmas has_derivative_within_subset = has_derivative_subset
 
+lemma has_derivative_within_singleton_iff:
+  "(f has_derivative g) (at x within {x}) \<longleftrightarrow> bounded_linear g"
+  by (auto intro!: has_derivativeI_sandwich[where e=1] has_derivative_bounded_linear)
+
+
+subsubsection \<open>Limit transformation for derivatives\<close>
+
+lemma has_derivative_transform_within:
+  assumes "(f has_derivative f') (at x within s)"
+    and "0 < d"
+    and "x \<in> s"
+    and "\<And>x'. \<lbrakk>x' \<in> s; dist x' x < d\<rbrakk> \<Longrightarrow> f x' = g x'"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+  unfolding has_derivative_within
+  by (force simp add: intro: Lim_transform_within)
+
+lemma has_derivative_transform_within_open:
+  assumes "(f has_derivative f') (at x within t)"
+    and "open s"
+    and "x \<in> s"
+    and "\<And>x. x\<in>s \<Longrightarrow> f x = g x"
+  shows "(g has_derivative f') (at x within t)"
+  using assms unfolding has_derivative_within
+  by (force simp add: intro: Lim_transform_within_open)
+
+lemma has_derivative_transform:
+  assumes "x \<in> s" "\<And>x. x \<in> s \<Longrightarrow> g x = f x"
+  assumes "(f has_derivative f') (at x within s)"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+  by (intro has_derivative_transform_within[OF _ zero_less_one, where g=g]) auto
+
+lemma has_derivative_transform_eventually:
+  assumes "(f has_derivative f') (at x within s)"
+    "(\<forall>\<^sub>F x' in at x within s. f x' = g x')"
+  assumes "f x = g x" "x \<in> s"
+  shows "(g has_derivative f') (at x within s)"
+  using assms
+proof -
+  from assms(2,3) obtain d where "d > 0" "\<And>x'. x' \<in> s \<Longrightarrow> dist x' x < d \<Longrightarrow> f x' = g x'"
+    by (force simp: eventually_at)
+  from has_derivative_transform_within[OF assms(1) this(1) assms(4) this(2)]
+  show ?thesis .
+qed
+
 
 subsection \<open>Continuity\<close>
 
@@ -295,6 +348,14 @@
   ((\<lambda>x. g (f x)) has_derivative (\<lambda>x. g' (f' x))) (at x within s)"
   by (blast intro: has_derivative_in_compose has_derivative_subset)
 
+lemma has_derivative_in_compose2:
+  assumes "\<And>x. x \<in> t \<Longrightarrow> (g has_derivative g' x) (at x within t)"
+  assumes "f ` s \<subseteq> t" "x \<in> s"
+  assumes "(f has_derivative f') (at x within s)"
+  shows "((\<lambda>x. g (f x)) has_derivative (\<lambda>y. g' (f x) (f' y))) (at x within s)"
+  using assms
+  by (auto intro: has_derivative_within_subset intro!: has_derivative_in_compose[of f f' x s g])
+
 lemma (in bounded_bilinear) FDERIV:
   assumes f: "(f has_derivative f') (at x within s)" and g: "(g has_derivative g') (at x within s)"
   shows "((\<lambda>x. f x ** g x) has_derivative (\<lambda>h. f x ** g' h + f' h ** g x)) (at x within s)"
@@ -467,6 +528,10 @@
 all directions. There is a proof in \<open>Analysis\<close> for \<open>euclidean_space\<close>.
 \<close>
 
+lemma has_derivative_at2: "(f has_derivative f') (at x) \<longleftrightarrow>
+    bounded_linear f' \<and> ((\<lambda>y. (1 / (norm(y - x))) *\<^sub>R (f y - (f x + f' (y - x)))) \<longlongrightarrow> 0) (at x)"
+  using has_derivative_within [of f f' x UNIV]
+  by simp
 lemma has_derivative_zero_unique:
   assumes "((\<lambda>x. 0) has_derivative F) (at x)"
   shows "F = (\<lambda>h. 0)"
@@ -542,10 +607,19 @@
     (\<lambda>x. f (g x)) differentiable (at x within s)"
   by (blast intro: differentiable_in_compose differentiable_subset)
 
-lemma differentiable_sum [simp, derivative_intros]:
+lemma differentiable_add [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> g differentiable F \<Longrightarrow> (\<lambda>x. f x + g x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_add)
 
+lemma differentiable_sum[simp, derivative_intros]:
+  assumes "finite s" "\<forall>a\<in>s. (f a) differentiable net"
+  shows "(\<lambda>x. sum (\<lambda>a. f a x) s) differentiable net"
+proof -
+  from bchoice[OF assms(2)[unfolded differentiable_def]]
+  show ?thesis
+    by (auto intro!: has_derivative_sum simp: differentiable_def)
+qed
+
 lemma differentiable_minus [simp, derivative_intros]:
   "f differentiable F \<Longrightarrow> (\<lambda>x. - f x) differentiable F"
   unfolding differentiable_def by (blast intro: has_derivative_minus)
@@ -651,6 +725,14 @@
   for c :: "'a::ab_semigroup_mult"
   by (simp add: fun_eq_iff mult.commute)
 
+lemma DERIV_compose_FDERIV:
+  fixes f::"real\<Rightarrow>real"
+  assumes "DERIV f (g x) :> f'"
+  assumes "(g has_derivative g') (at x within s)"
+  shows "((\<lambda>x. f (g x)) has_derivative (\<lambda>x. g' x * f')) (at x within s)"
+  using assms has_derivative_compose[of g g' x s f "( * ) f'"]
+  by (auto simp: has_field_derivative_def ac_simps)
+
 
 subsection \<open>Vector derivative\<close>
 
@@ -998,6 +1080,8 @@
     by eventually_elim auto
 qed
 
+lemmas has_derivative_floor[derivative_intros] =
+  floor_has_real_derivative[THEN DERIV_compose_FDERIV]
 
 text \<open>Caratheodory formulation of derivative at a point\<close>
 
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -1800,8 +1800,176 @@
 lemma max_MInf2 [simp]: "max x (-\<infinity>::ereal) = x"
 by (metis max_bot2 bot_ereal_def)
 
-
-subsubsection "Topological space"
+subsection \<open>Extended real intervals\<close>
+
+lemma real_greaterThanLessThan_infinity_eq:
+  "real_of_ereal ` {N::ereal<..<\<infinity>} =
+    (if N = \<infinity> then {} else if N = -\<infinity> then UNIV else {real_of_ereal N<..})"
+proof -
+  {
+    fix x::real
+    have "x \<in> real_of_ereal ` {- \<infinity><..<\<infinity>::ereal}"
+      by (auto intro!: image_eqI[where x="ereal x"])
+  } moreover {
+    fix x::ereal
+    assume "N \<noteq> - \<infinity>" "N < x" "x \<noteq> \<infinity>"
+    then have "real_of_ereal N < real_of_ereal x"
+      by (cases N; cases x; simp)
+  } moreover {
+    fix x::real
+    assume "N \<noteq> \<infinity>" "real_of_ereal N < x"
+    then have "x \<in> real_of_ereal ` {N<..<\<infinity>}"
+      by (cases N) (auto intro!: image_eqI[where x="ereal x"])
+  } ultimately show ?thesis by auto
+qed
+
+lemma real_greaterThanLessThan_minus_infinity_eq:
+  "real_of_ereal ` {-\<infinity><..<N::ereal} =
+    (if N = \<infinity> then UNIV else if N = -\<infinity> then {} else {..<real_of_ereal N})"
+proof -
+  have "real_of_ereal ` {-\<infinity><..<N::ereal} = uminus ` real_of_ereal ` {-N<..<\<infinity>}"
+    by (auto simp: ereal_uminus_less_reorder intro!: image_eqI[where x="-x" for x])
+  also note real_greaterThanLessThan_infinity_eq
+  finally show ?thesis by (auto intro!: image_eqI[where x="-x" for x])
+qed
+
+lemma real_greaterThanLessThan_inter:
+  "real_of_ereal ` {N<..<M::ereal} = real_of_ereal ` {-\<infinity><..<M} \<inter> real_of_ereal ` {N<..<\<infinity>}"
+  apply safe
+  subgoal by force
+  subgoal by force
+  subgoal for x y z
+    by (cases y; cases z) (auto intro!: image_eqI[where x=z] simp: )
+  done
+
+lemma real_atLeastGreaterThan_eq: "real_of_ereal ` {N<..<M::ereal} =
+   (if N = \<infinity> then {} else
+   if N = -\<infinity> then
+    (if M = \<infinity> then UNIV
+    else if M = -\<infinity> then {}
+    else {..< real_of_ereal M})
+  else if M = - \<infinity> then {}
+  else if M = \<infinity> then {real_of_ereal N<..}
+  else {real_of_ereal N <..< real_of_ereal M})"
+  apply (subst real_greaterThanLessThan_inter)
+  apply (subst real_greaterThanLessThan_minus_infinity_eq)
+  apply (subst real_greaterThanLessThan_infinity_eq)
+  apply auto
+  done
+
+lemma real_image_ereal_ivl:
+  fixes a b::ereal
+  shows
+  "real_of_ereal ` {a<..<b} =
+  (if a < b then (if a = - \<infinity> then if b = \<infinity> then UNIV else {..<real_of_ereal b}
+  else if b = \<infinity> then {real_of_ereal a<..} else {real_of_ereal a <..< real_of_ereal b}) else {})"
+  by (cases a; cases b; simp add: real_atLeastGreaterThan_eq not_less)
+
+lemma fixes a b c::ereal
+  shows not_inftyI: "a < b \<Longrightarrow> b < c \<Longrightarrow> abs b \<noteq> \<infinity>"
+  by force
+
+lemma
+  interval_neqs:
+  fixes r s t::real
+  shows "{r<..<s} \<noteq> {t<..}"
+    and "{r<..<s} \<noteq> {..<t}"
+    and "{r<..<ra} \<noteq> UNIV"
+    and "{r<..} \<noteq> {..<s}"
+    and "{r<..} \<noteq> UNIV"
+    and "{..<r} \<noteq> UNIV"
+    and "{} \<noteq> {r<..}"
+    and "{} \<noteq> {..<r}"
+  subgoal
+    by (metis dual_order.strict_trans greaterThanLessThan_iff greaterThan_iff gt_ex not_le order_refl)
+  subgoal
+    by (metis (no_types, hide_lams) greaterThanLessThan_empty_iff greaterThanLessThan_iff gt_ex
+        lessThan_iff minus_minus neg_less_iff_less not_less order_less_irrefl)
+  subgoal by force
+  subgoal
+    by (metis greaterThanLessThan_empty_iff greaterThanLessThan_eq greaterThan_iff inf.idem
+        lessThan_iff lessThan_non_empty less_irrefl not_le)
+  subgoal by force
+  subgoal by force
+  subgoal using greaterThan_non_empty by blast
+  subgoal using lessThan_non_empty by blast
+  done
+
+lemma greaterThanLessThan_eq_iff:
+  fixes r s t u::real
+  shows "({r<..<s} = {t<..<u}) = (r \<ge> s \<and> u \<le> t \<or> r = t \<and> s = u)"
+  by (metis cInf_greaterThanLessThan cSup_greaterThanLessThan greaterThanLessThan_empty_iff not_le)
+
+lemma real_of_ereal_image_greaterThanLessThan_iff:
+  "real_of_ereal ` {a <..< b} = real_of_ereal ` {c <..< d} \<longleftrightarrow> (a \<ge> b \<and> c \<ge> d \<or> a = c \<and> b = d)"
+  unfolding real_atLeastGreaterThan_eq
+  by (cases a; cases b; cases c; cases d;
+    simp add: greaterThanLessThan_eq_iff interval_neqs interval_neqs[symmetric])
+
+lemma uminus_image_real_of_ereal_image_greaterThanLessThan:
+  "uminus ` real_of_ereal ` {l <..< u} = real_of_ereal ` {-u <..< -l}"
+  by (force simp: algebra_simps ereal_less_uminus_reorder
+    ereal_uminus_less_reorder intro: image_eqI[where x="-x" for x])
+
+lemma add_image_real_of_ereal_image_greaterThanLessThan:
+  "(+) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c + l <..< c + u}"
+  apply safe
+  subgoal for x
+    using ereal_less_add[of c]
+    by (force simp: real_of_ereal_add add.commute)
+  subgoal for _ x
+    by (force simp: add.commute real_of_ereal_minus ereal_minus_less ereal_less_minus
+      intro: image_eqI[where x="x - c"])
+  done
+
+lemma add2_image_real_of_ereal_image_greaterThanLessThan:
+  "(\<lambda>x. x + c) ` real_of_ereal ` {l <..< u} = real_of_ereal ` {l + c <..< u + c}"
+  using add_image_real_of_ereal_image_greaterThanLessThan[of c l u]
+  by (metis add.commute image_cong)
+
+lemma minus_image_real_of_ereal_image_greaterThanLessThan:
+  "(-) c ` real_of_ereal ` {l <..< u} = real_of_ereal ` {c - u <..< c - l}"
+  (is "?l = ?r")
+proof -
+  have "?l = (+) c ` uminus ` real_of_ereal ` {l <..< u}" by auto
+  also note uminus_image_real_of_ereal_image_greaterThanLessThan
+  also note add_image_real_of_ereal_image_greaterThanLessThan
+  finally show ?thesis by (simp add: minus_ereal_def)
+qed
+
+lemma real_ereal_bound_lemma_up:
+  assumes "s \<in> real_of_ereal ` {a<..<b}"
+  assumes "t \<notin> real_of_ereal ` {a<..<b}"
+  assumes "s \<le> t"
+  shows "b \<noteq> \<infinity>"
+  using assms
+  apply (cases b)
+  subgoal by force
+  subgoal by (metis PInfty_neq_ereal(2) assms dual_order.strict_trans1 ereal_infty_less(1)
+    ereal_less_ereal_Ex greaterThanLessThan_empty_iff greaterThanLessThan_iff greaterThan_iff
+    image_eqI less_imp_le linordered_field_no_ub not_less order_trans
+    real_greaterThanLessThan_infinity_eq real_image_ereal_ivl real_of_ereal.simps(1))
+  subgoal by force
+  done
+
+lemma real_ereal_bound_lemma_down:
+  assumes "s \<in> real_of_ereal ` {a<..<b}"
+  assumes "t \<notin> real_of_ereal ` {a<..<b}"
+  assumes "t \<le> s"
+  shows "a \<noteq> - \<infinity>"
+  using assms
+  apply (cases b)
+  subgoal
+    apply safe
+    using assms(1)
+    apply (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+    done
+  subgoal by (auto simp: real_greaterThanLessThan_minus_infinity_eq)
+  subgoal by auto
+  done
+
+
+subsection "Topological space"
 
 instantiation ereal :: linear_continuum_topology
 begin
@@ -2469,6 +2637,21 @@
      by auto
 qed (auto simp add: image_Union image_Int)
 
+lemma open_image_real_of_ereal:
+  fixes X::"ereal set"
+  assumes "open X"
+  assumes "\<infinity> \<notin> X"
+  assumes "-\<infinity> \<notin> X"
+  shows "open (real_of_ereal ` X)"
+proof -
+  have "real_of_ereal ` X = ereal -` X"
+    apply safe
+    subgoal by (metis assms(2) assms(3) real_of_ereal.elims vimageI)
+    subgoal using image_iff by fastforce
+    done
+  thus ?thesis
+    by (auto intro!: open_ereal_vimage assms)
+qed
 
 lemma eventually_finite:
   fixes x :: ereal
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Limits.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -52,6 +52,9 @@
   for f :: "_ \<Rightarrow> real"
   by (rule filterlim_mono[OF _ at_top_le_at_infinity order_refl])
 
+lemma filterlim_real_at_infinity_sequentially: "filterlim real at_infinity sequentially"
+  by (simp add: filterlim_at_top_imp_at_infinity filterlim_real_sequentially)
+
 lemma lim_infinity_imp_sequentially: "(f \<longlongrightarrow> l) at_infinity \<Longrightarrow> ((\<lambda>n. f(n)) \<longlongrightarrow> l) sequentially"
   by (simp add: filterlim_at_top_imp_at_infinity filterlim_compose filterlim_real_sequentially)
 
@@ -1256,6 +1259,20 @@
   for a :: real
   unfolding at_right_to_0[of a] by (simp add: eventually_filtermap)
 
+lemma at_to_0: "at a = filtermap (\<lambda>x. x + a) (at 0)"
+  for a :: "'a::real_normed_vector"
+  using filtermap_at_shift[of "-a" 0] by simp
+
+lemma filterlim_at_to_0:
+  "filterlim f F (at a) \<longleftrightarrow> filterlim (\<lambda>x. f (x + a)) F (at 0)"
+  for a :: "'a::real_normed_vector"
+  unfolding filterlim_def filtermap_filtermap at_to_0[of a] ..
+
+lemma eventually_at_to_0:
+  "eventually P (at a) \<longleftrightarrow> eventually (\<lambda>x. P (x + a)) (at 0)"
+  for a ::  "'a::real_normed_vector"
+  unfolding at_to_0[of a] by (simp add: eventually_filtermap)
+
 lemma filtermap_at_minus: "filtermap (\<lambda>x. - x) (at a) = at (- a)"
   for a :: "'a::real_normed_vector"
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
@@ -1268,6 +1285,7 @@
   for a :: real
   by (simp add: filter_eq_iff eventually_filtermap eventually_at_filter filtermap_nhds_minus[symmetric])
 
+
 lemma filterlim_at_left_to_right:
   "filterlim f F (at_left a) \<longleftrightarrow> filterlim (\<lambda>x. f (- x)) F (at_right (-a))"
   for a :: real
@@ -1486,6 +1504,36 @@
   for c :: nat
   by (rule filterlim_subseq) (auto simp: strict_mono_def)
 
+lemma filterlim_times_pos:
+  "LIM x F1. c * f x :> at_right l"
+  if "filterlim f (at_right p) F1" "0 < c" "l = c * p"
+  for c::"'a::{linordered_field, linorder_topology}"
+  unfolding filterlim_iff
+proof safe
+  fix P
+  assume "\<forall>\<^sub>F x in at_right l. P x"
+  then obtain d where "c * p < d" "\<And>y. y > c * p \<Longrightarrow> y < d \<Longrightarrow> P y"
+    unfolding \<open>l = _ \<close> eventually_at_right_field
+    by auto
+  then have "\<forall>\<^sub>F a in at_right p. P (c * a)"
+    by (auto simp: eventually_at_right_field \<open>0 < c\<close> field_simps intro!: exI[where x="d/c"])
+  from that(1)[unfolded filterlim_iff, rule_format, OF this]
+  show "\<forall>\<^sub>F x in F1. P (c * f x)" .
+qed
+
+lemma filtermap_nhds_times: "c \<noteq> 0 \<Longrightarrow> filtermap (times c) (nhds a) = nhds (c * a)"
+  for a c :: "'a::real_normed_field"
+  by (rule filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+    (auto intro!: tendsto_eq_intros filterlim_ident)
+
+lemma filtermap_times_pos_at_right:
+  fixes c::"'a::{linordered_field, linorder_topology}"
+  assumes "c > 0"
+  shows "filtermap (times c) (at_right p) = at_right (c * p)"
+  using assms
+  by (intro filtermap_fun_inverse[where g="\<lambda>x. inverse c * x"])
+    (auto intro!: filterlim_ident filterlim_times_pos)
+
 lemma at_to_infinity: "(at (0::'a::{real_normed_field,field})) = filtermap inverse at_infinity"
 proof (rule antisym)
   have "(inverse \<longlongrightarrow> (0::'a)) at_infinity"
@@ -1936,6 +1984,10 @@
 lemma lim_inverse_n: "((\<lambda>n. inverse(of_nat n)) \<longlongrightarrow> (0::'a::real_normed_field)) sequentially"
   using lim_1_over_n by (simp add: inverse_eq_divide)
 
+lemma lim_inverse_n': "((\<lambda>n. 1 / n) \<longlongrightarrow> 0) sequentially"
+  using lim_inverse_n
+  by (simp add: inverse_eq_divide)
+
 lemma LIMSEQ_Suc_n_over_n: "(\<lambda>n. of_nat (Suc n) / of_nat n :: 'a :: real_normed_field) \<longlonglongrightarrow> 1"
 proof (rule Lim_transform_eventually)
   show "eventually (\<lambda>n. 1 + inverse (of_nat n :: 'a) = of_nat (Suc n) / of_nat n) sequentially"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/NthRoot.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -480,6 +480,9 @@
 lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
   by (meson not_le real_less_rsqrt)
 
+lemma sqrt_ge_absD: "\<bar>x\<bar> \<le> sqrt y \<Longrightarrow> x\<^sup>2 \<le> y"
+  using real_sqrt_le_iff[of "x\<^sup>2"] by simp
+
 lemma sqrt_even_pow2:
   assumes n: "even n"
   shows "sqrt (2 ^ n) = 2 ^ (n div 2)"
@@ -538,6 +541,8 @@
   DERIV_real_sqrt_generic[THEN DERIV_chain2, derivative_intros]
   DERIV_real_root_generic[THEN DERIV_chain2, derivative_intros]
 
+lemmas has_derivative_real_sqrt[derivative_intros] = DERIV_real_sqrt[THEN DERIV_compose_FDERIV]
+
 lemma not_real_square_gt_zero [simp]: "\<not> 0 < x * x \<longleftrightarrow> x = 0"
   for x :: real
   apply auto
@@ -658,6 +663,13 @@
 lemma le_real_sqrt_sumsq [simp]: "x \<le> sqrt (x * x + y * y)"
   by (simp add: power2_eq_square [symmetric])
 
+lemma sqrt_sum_squares_le_sum:
+  "\<lbrakk>0 \<le> x; 0 \<le> y\<rbrakk> \<Longrightarrow> sqrt (x\<^sup>2 + y\<^sup>2) \<le> x + y"
+  apply (rule power2_le_imp_le)
+  apply (simp add: power2_sum)
+  apply simp
+  done
+
 lemma real_sqrt_sum_squares_triangle_ineq:
   "sqrt ((a + c)\<^sup>2 + (b + d)\<^sup>2) \<le> sqrt (a\<^sup>2 + b\<^sup>2) + sqrt (c\<^sup>2 + d\<^sup>2)"
   apply (rule power2_le_imp_le)
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Set_Interval.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -222,6 +222,10 @@
   "{a..<b} = {a..b} - {b}"
   by (auto simp add: atLeastLessThan_def atLeastAtMost_def)
 
+lemma (in order) greaterThanAtMost_eq_atLeastAtMost_diff:
+  "{a<..b} = {a..b} - {a}"
+  by (auto simp add: greaterThanAtMost_def atLeastAtMost_def)
+
 end
 
 subsubsection\<open>Emptyness, singletons, subset\<close>
@@ -869,6 +873,19 @@
 context linordered_semidom
 begin
 
+lemma image_add_atLeast[simp]: "plus k ` {i..} = {k + i..}"
+proof -
+  have "n = k + (n - k)" if "i + k \<le> n" for n
+  proof -
+    have "n = (n - (k + i)) + (k + i)" using that
+      by (metis add_commute le_add_diff_inverse)
+    then show "n = k + (n - k)"
+      by (metis local.add_diff_cancel_left' add_assoc add_commute)
+  qed
+  then show ?thesis
+    by (fastforce simp: add_le_imp_le_diff add.commute)
+qed
+
 lemma image_add_atLeastAtMost [simp]:
   "plus k ` {i..j} = {i + k..j + k}" (is "?A = ?B")
 proof
@@ -911,112 +928,11 @@
   "(\<lambda>n. n + k) ` {i..<j} = {i + k..<j + k}"
   by (simp add: add.commute [of _ k])
 
+lemma image_add_greaterThanAtMost[simp]: "(+) c ` {a<..b} = {c + a<..c + b}"
+  by (simp add: image_set_diff greaterThanAtMost_eq_atLeastAtMost_diff ac_simps)
+
 end
 
-lemma image_Suc_atLeastAtMost [simp]:
-  "Suc ` {i..j} = {Suc i..Suc j}"
-  using image_add_atLeastAtMost [of 1 i j]
-    by (simp only: plus_1_eq_Suc) simp
-
-lemma image_Suc_atLeastLessThan [simp]:
-  "Suc ` {i..<j} = {Suc i..<Suc j}"
-  using image_add_atLeastLessThan [of 1 i j]
-    by (simp only: plus_1_eq_Suc) simp
-
-corollary image_Suc_atMost:
-  "Suc ` {..n} = {1..Suc n}"
-  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-
-corollary image_Suc_lessThan:
-  "Suc ` {..<n} = {1..n}"
-  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
-  
-lemma image_diff_atLeastAtMost [simp]:
-  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
-  apply auto
-  apply (rule_tac x="d-x" in rev_image_eqI, auto)
-  done
-
-lemma image_mult_atLeastAtMost [simp]:
-  fixes d::"'a::linordered_field"
-  assumes "d>0" shows "(( * ) d ` {a..b}) = {d*a..d*b}"
-  using assms
-  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
-
-lemma image_affinity_atLeastAtMost:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a + c .. m *b + c}
-            else {m*b + c .. m*a + c})"
-  apply (case_tac "m=0", auto simp: mult_le_cancel_left)
-  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
-  apply (rule_tac x="inverse m*(x-c)" in rev_image_eqI, auto simp: field_simps)
-  done
-
-lemma image_affinity_atLeastAtMost_diff:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {m*a - c .. m*b - c}
-            else {m*b - c .. m*a - c})"
-  using image_affinity_atLeastAtMost [of m "-c" a b]
-  by simp
-
-lemma image_affinity_atLeastAtMost_div:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m + c .. b/m + c}
-            else {b/m + c .. a/m + c})"
-  using image_affinity_atLeastAtMost [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma image_affinity_atLeastAtMost_div_diff:
-  fixes c :: "'a::linordered_field"
-  shows "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
-            else if 0 \<le> m then {a/m - c .. b/m - c}
-            else {b/m - c .. a/m - c})"
-  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
-  by (simp add: field_class.field_divide_inverse algebra_simps)
-
-lemma atLeast1_lessThan_eq_remove0:
-  "{Suc 0..<n} = {..<n} - {0}"
-  by auto
-
-lemma atLeast1_atMost_eq_remove0:
-  "{Suc 0..n} = {..n} - {0}"
-  by auto
-
-lemma image_add_int_atLeastLessThan:
-    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
-  apply (auto simp add: image_def)
-  apply (rule_tac x = "x - l" in bexI)
-  apply auto
-  done
-
-lemma image_minus_const_atLeastLessThan_nat:
-  fixes c :: nat
-  shows "(\<lambda>i. i - c) ` {x ..< y} =
-      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
-    (is "_ = ?right")
-proof safe
-  fix a assume a: "a \<in> ?right"
-  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
-  proof cases
-    assume "c < y" with a show ?thesis
-      by (auto intro!: image_eqI[of _ _ "a + c"])
-  next
-    assume "\<not> c < y" with a show ?thesis
-      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
-  qed
-qed auto
-
-lemma image_int_atLeastLessThan:
-  "int ` {a..<b} = {int a..<int b}"
-  by (auto intro!: image_eqI [where x = "nat x" for x])
-
-lemma image_int_atLeastAtMost:
-  "int ` {a..b} = {int a..int b}"
-  by (auto intro!: image_eqI [where x = "nat x" for x])
-
 context ordered_ab_group_add
 begin
 
@@ -1057,8 +973,184 @@
   and image_uminus_greaterThanLessThan[simp]: "uminus ` {x<..<y} = {-y<..<-x}"
   by (simp_all add: atLeastAtMost_def greaterThanAtMost_def atLeastLessThan_def
       greaterThanLessThan_def image_Int[OF inj_uminus] Int_commute)
+
+lemma image_add_atMost[simp]: "(+) c ` {..a} = {..c + a}"
+  by (auto intro!: image_eqI[where x="x - c" for x] simp: algebra_simps)
+
 end
 
+lemma image_Suc_atLeastAtMost [simp]:
+  "Suc ` {i..j} = {Suc i..Suc j}"
+  using image_add_atLeastAtMost [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+lemma image_Suc_atLeastLessThan [simp]:
+  "Suc ` {i..<j} = {Suc i..<Suc j}"
+  using image_add_atLeastLessThan [of 1 i j]
+    by (simp only: plus_1_eq_Suc) simp
+
+corollary image_Suc_atMost:
+  "Suc ` {..n} = {1..Suc n}"
+  by (simp add: atMost_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+corollary image_Suc_lessThan:
+  "Suc ` {..<n} = {1..n}"
+  by (simp add: lessThan_atLeast0 atLeastLessThanSuc_atLeastAtMost)
+
+lemma image_diff_atLeastAtMost [simp]:
+  fixes d::"'a::linordered_idom" shows "((-) d ` {a..b}) = {d-b..d-a}"
+  apply auto
+  apply (rule_tac x="d-x" in rev_image_eqI, auto)
+  done
+
+lemma image_diff_atLeastLessThan [simp]:
+  fixes a b c::"'a::linordered_idom"
+  shows "(-) c ` {a..<b} = {c - b<..c - a}"
+proof -
+  have "(-) c ` {a..<b} = (+) c ` uminus ` {a ..<b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b<..c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_greaterThanAtMost_real[simp]:
+  fixes a b c::"'a::linordered_idom"
+  shows "(-) c ` {a<..b} = {c - b..<c - a}"
+proof -
+  have "(-) c ` {a<..b} = (+) c ` uminus ` {a<..b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b..<c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_atLeast_real[simp]:
+  fixes a c::"'a::linordered_idom"
+  shows "(-) c ` {a..} = {..c - a}"
+proof -
+  have "(-) c ` {a..} = (+) c ` uminus ` {a ..}"
+    unfolding image_image by simp
+  also have "\<dots> = {..c - a}" by simp
+  finally show ?thesis by simp
+qed
+
+lemma image_minus_const_AtMost_real[simp]:
+  fixes b c::"'a::linordered_idom"
+  shows "(-) c ` {..b} = {c - b..}"
+proof -
+  have "(-) c ` {..b} = (+) c ` uminus ` {..b}"
+    unfolding image_image by simp
+  also have "\<dots> = {c - b..}" by simp
+  finally show ?thesis by simp
+qed
+
+context linordered_field begin
+
+lemma image_mult_atLeastAtMost [simp]:
+  "(( * ) d ` {a..b}) = {d*a..d*b}" if "d>0"
+  using that
+  by (auto simp: field_simps mult_le_cancel_right intro: rev_image_eqI [where x="x/d" for x])
+
+lemma image_mult_atLeastAtMost_if:
+  "( * ) c ` {x .. y} =
+    (if c > 0 then {c * x .. c * y} else if x \<le> y then {c * y .. c * x} else {})"
+proof -
+  consider "c < 0" "x \<le> y" | "c = 0" "x \<le> y" | "c > 0" "x \<le> y" | "x > y"
+    using local.antisym_conv3 local.leI by blast
+  then show ?thesis
+  proof cases
+    case 1
+    have "( * ) c ` {x .. y} = uminus ` ( * ) (- c) ` {x .. y}"
+      by (simp add: image_image)
+    also have "\<dots> = {c * y .. c * x}"
+      using \<open>c < 0\<close>
+      by simp
+    finally show ?thesis
+      using \<open>c < 0\<close> by auto
+  qed (auto simp: not_le local.mult_less_cancel_left_pos)
+qed
+
+lemma image_mult_atLeastAtMost_if':
+  "(\<lambda>x. x * c) ` {x..y} =
+    (if x \<le> y then if c > 0 then {x * c .. y * c} else {y * c .. x * c} else {})"
+  by (subst mult.commute)
+    (simp add: image_mult_atLeastAtMost_if mult.commute mult_le_cancel_left_pos)
+
+lemma image_affinity_atLeastAtMost:
+  "((\<lambda>x. m*x + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {m*a + c .. m *b + c}
+            else {m*b + c .. m*a + c})"
+proof -
+  have "(\<lambda>x. m*x + c) = ((\<lambda>x. x + c) o ( * ) m)"
+    unfolding image_comp[symmetric]
+    by (simp add: o_def)
+  then show ?thesis
+    by (auto simp add: image_comp[symmetric] image_mult_atLeastAtMost_if mult_le_cancel_left)
+qed
+
+lemma image_affinity_atLeastAtMost_diff:
+  "((\<lambda>x. m*x - c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {m*a - c .. m*b - c}
+            else {m*b - c .. m*a - c})"
+  using image_affinity_atLeastAtMost [of m "-c" a b]
+  by simp
+
+lemma image_affinity_atLeastAtMost_div:
+  "((\<lambda>x. x/m + c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m + c .. b/m + c}
+            else {b/m + c .. a/m + c})"
+  using image_affinity_atLeastAtMost [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+lemma image_affinity_atLeastAtMost_div_diff:
+  "((\<lambda>x. x/m - c) ` {a..b}) = (if {a..b}={} then {}
+            else if 0 \<le> m then {a/m - c .. b/m - c}
+            else {b/m - c .. a/m - c})"
+  using image_affinity_atLeastAtMost_diff [of "inverse m" c a b]
+  by (simp add: field_class.field_divide_inverse algebra_simps inverse_eq_divide)
+
+end
+
+lemma atLeast1_lessThan_eq_remove0:
+  "{Suc 0..<n} = {..<n} - {0}"
+  by auto
+
+lemma atLeast1_atMost_eq_remove0:
+  "{Suc 0..n} = {..n} - {0}"
+  by auto
+
+lemma image_add_int_atLeastLessThan:
+    "(%x. x + (l::int)) ` {0..<u-l} = {l..<u}"
+  apply (auto simp add: image_def)
+  apply (rule_tac x = "x - l" in bexI)
+  apply auto
+  done
+
+lemma image_minus_const_atLeastLessThan_nat:
+  fixes c :: nat
+  shows "(\<lambda>i. i - c) ` {x ..< y} =
+      (if c < y then {x - c ..< y - c} else if x < y then {0} else {})"
+    (is "_ = ?right")
+proof safe
+  fix a assume a: "a \<in> ?right"
+  show "a \<in> (\<lambda>i. i - c) ` {x ..< y}"
+  proof cases
+    assume "c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ "a + c"])
+  next
+    assume "\<not> c < y" with a show ?thesis
+      by (auto intro!: image_eqI[of _ _ x] split: if_split_asm)
+  qed
+qed auto
+
+lemma image_int_atLeastLessThan:
+  "int ` {a..<b} = {int a..<int b}"
+  by (auto intro!: image_eqI [where x = "nat x" for x])
+
+lemma image_int_atLeastAtMost:
+  "int ` {a..b} = {int a..int b}"
+  by (auto intro!: image_eqI [where x = "nat x" for x])
+
+
 subsubsection \<open>Finiteness\<close>
 
 lemma finite_lessThan [iff]: fixes k :: nat shows "finite {..<k}"
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -609,7 +609,6 @@
     and "filterlim g G (at x within {x. \<not>P x})"
   shows "filterlim (\<lambda>x. if P x then f x else g x) G (at x)"
   using assms by (intro filterlim_at_within_If) simp_all
-
 lemma (in linorder_topology) at_within_order:
   assumes "UNIV \<noteq> {x}"
   shows "at x within s =
@@ -692,7 +691,18 @@
      (\<exists>S. open S \<and> A \<in> S \<and> (\<forall>x. f x \<in> S \<inter> B - {A} \<longrightarrow> P x))" (is "?lhs = ?rhs")
   unfolding at_within_def filtercomap_inf eventually_inf_principal filtercomap_principal 
           eventually_filtercomap_nhds eventually_principal by blast
-    
+
+lemma eventually_at_right_field:
+  "eventually P (at_right x) \<longleftrightarrow> (\<exists>b>x. \<forall>y>x. y < b \<longrightarrow> P y)"
+  for x :: "'a::{linordered_field, linorder_topology}"
+  using linordered_field_no_ub[rule_format, of x]
+  by (auto simp: eventually_at_right)
+
+lemma eventually_at_left_field:
+  "eventually P (at_left x) \<longleftrightarrow> (\<exists>b<x. \<forall>y>b. y < x \<longrightarrow> P y)"
+  for x :: "'a::{linordered_field, linorder_topology}"
+  using linordered_field_no_lb[rule_format, of x]
+  by (auto simp: eventually_at_left)
 
 
 subsubsection \<open>Tendsto\<close>
@@ -762,9 +772,11 @@
 
 end
 
-lemma tendsto_within_subset:
-  "(f \<longlongrightarrow> l) (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> (f \<longlongrightarrow> l) (at x within T)"
-  by (blast intro: tendsto_mono at_le)
+lemma (in topological_space) filterlim_within_subset:
+  "filterlim f l (at x within S) \<Longrightarrow> T \<subseteq> S \<Longrightarrow> filterlim f l (at x within T)"
+  by (blast intro: filterlim_mono at_le)
+
+lemmas tendsto_within_subset = filterlim_within_subset
 
 lemma (in order_topology) order_tendsto_iff:
   "(f \<longlongrightarrow> x) F \<longleftrightarrow> (\<forall>l<x. eventually (\<lambda>x. l < f x) F) \<and> (\<forall>u>x. eventually (\<lambda>x. f x < u) F)"
@@ -963,6 +975,11 @@
 lemma Lim_ident_at: "\<not> trivial_limit (at x within s) \<Longrightarrow> Lim (at x within s) (\<lambda>x. x) = x"
   by (rule tendsto_Lim[OF _ tendsto_ident_at]) auto
 
+lemma eventually_Lim_ident_at:
+  "(\<forall>\<^sub>F y in at x within X. P (Lim (at x within X) (\<lambda>x. x)) y) \<longleftrightarrow>
+    (\<forall>\<^sub>F y in at x within X. P x y)" for x::"'a::t2_space"
+  by (cases "at x within X = bot") (auto simp: Lim_ident_at)
+
 lemma filterlim_at_bot_at_right:
   fixes f :: "'a::linorder_topology \<Rightarrow> 'b::linorder"
   assumes mono: "\<And>x y. Q x \<Longrightarrow> Q y \<Longrightarrow> x \<le> y \<Longrightarrow> f x \<le> f y"
@@ -2612,6 +2629,37 @@
     by (metis less_le)
 qed
 
+lemma (in linorder_topology) not_in_connected_cases:
+  assumes conn: "connected S"
+  assumes nbdd: "x \<notin> S"
+  assumes ne: "S \<noteq> {}"
+  obtains "bdd_above S" "\<And>y. y \<in> S \<Longrightarrow> x \<ge> y" | "bdd_below S" "\<And>y. y \<in> S \<Longrightarrow> x \<le> y"
+proof -
+  obtain s where "s \<in> S" using ne by blast
+  {
+    assume "s \<le> x"
+    have "False" if "x \<le> y" "y \<in> S" for y
+      using connectedD_interval[OF conn \<open>s \<in> S\<close> \<open>y \<in> S\<close> \<open>s \<le> x\<close> \<open>x \<le> y\<close>] \<open>x \<notin> S\<close>
+      by simp
+    then have wit: "y \<in> S \<Longrightarrow> x \<ge> y" for y
+      using le_cases by blast
+    then have "bdd_above S"
+      by (rule local.bdd_aboveI)
+    note this wit
+  } moreover {
+    assume "x \<le> s"
+    have "False" if "x \<ge> y" "y \<in> S" for y
+      using connectedD_interval[OF conn \<open>y \<in> S\<close> \<open>s \<in> S\<close> \<open>x \<ge> y\<close> \<open>s \<ge> x\<close> ] \<open>x \<notin> S\<close>
+      by simp
+    then have wit: "y \<in> S \<Longrightarrow> x \<le> y" for y
+      using le_cases by blast
+    then have "bdd_below S"
+      by (rule bdd_belowI)
+    note this wit
+  } ultimately show ?thesis
+    by (meson le_cases that)
+qed
+
 lemma connected_continuous_image:
   assumes *: "continuous_on s f"
     and "connected s"
@@ -3454,6 +3502,15 @@
 lemma isCont_Pair [simp]: "\<lbrakk>isCont f a; isCont g a\<rbrakk> \<Longrightarrow> isCont (\<lambda>x. (f x, g x)) a"
   by (fact continuous_Pair)
 
+lemma continuous_on_compose_Pair:
+  assumes f: "continuous_on (Sigma A B) (\<lambda>(a, b). f a b)"
+  assumes g: "continuous_on C g"
+  assumes h: "continuous_on C h"
+  assumes subset: "\<And>c. c \<in> C \<Longrightarrow> g c \<in> A" "\<And>c. c \<in> C \<Longrightarrow> h c \<in> B (g c)"
+  shows "continuous_on C (\<lambda>c. f (g c) (h c))"
+  using continuous_on_compose2[OF f continuous_on_Pair[OF g h]] subset
+  by auto
+
 
 subsubsection \<open>Connectedness of products\<close>
 
diff -r 00c436488398 -r bdff8bf0a75b src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Tue Feb 20 22:25:23 2018 +0100
+++ b/src/HOL/Transcendental.thy	Thu Feb 22 15:17:25 2018 +0100
@@ -1389,6 +1389,8 @@
 declare DERIV_exp[THEN DERIV_chain2, derivative_intros]
   and DERIV_exp[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_exp[derivative_intros] = DERIV_exp[THEN DERIV_compose_FDERIV]
+
 lemma norm_exp: "norm (exp x) \<le> exp (norm x)"
 proof -
   from summable_norm[OF summable_norm_exp, of x]
@@ -1883,6 +1885,8 @@
 declare DERIV_ln_divide[THEN DERIV_chain2, derivative_intros]
   and DERIV_ln_divide[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_ln[derivative_intros] = DERIV_ln[THEN DERIV_compose_FDERIV]
+
 lemma ln_series:
   assumes "0 < x" and "x < 2"
   shows "ln x = (\<Sum> n. (-1)^n * (1 / real (n + 1)) * (x - 1)^(Suc n))"
@@ -3094,24 +3098,33 @@
   shows "((\<lambda>x. f x powr g x) \<longlongrightarrow> a powr b) F"
   using tendsto_powr'[of f a F g b] assms by auto
 
+lemma has_derivative_powr[derivative_intros]:
+  assumes g[derivative_intros]: "(g has_derivative g') (at x within X)"
+    and f[derivative_intros]:"(f has_derivative f') (at x within X)"
+  assumes pos: "0 < g x" and "x \<in> X"
+  shows "((\<lambda>x. g x powr f x::real) has_derivative (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+proof -
+  have "\<forall>\<^sub>F x in at x within X. g x > 0"
+    by (rule order_tendstoD[OF _ pos])
+      (rule has_derivative_continuous[OF g, unfolded continuous_within])
+  then obtain d where "d > 0" and pos': "\<And>x'. x' \<in> X \<Longrightarrow> dist x' x < d \<Longrightarrow> 0 < g x'"
+    using pos unfolding eventually_at by force
+  have "((\<lambda>x. exp (f x * ln (g x))) has_derivative
+    (\<lambda>h. (g x powr f x) * (f' h * ln (g x) + g' h * f x / g x))) (at x within X)"
+    using pos
+    by (auto intro!: derivative_eq_intros simp: divide_simps powr_def)
+  then show ?thesis
+    by (rule has_derivative_transform_within[OF _ \<open>d > 0\<close> \<open>x \<in> X\<close>]) (auto simp: powr_def dest: pos')
+qed
+
 lemma DERIV_powr:
   fixes r :: real
   assumes g: "DERIV g x :> m"
     and pos: "g x > 0"
     and f: "DERIV f x :> r"
   shows "DERIV (\<lambda>x. g x powr f x) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
-proof -
-  have "DERIV (\<lambda>x. exp (f x * ln (g x))) x :> (g x powr f x) * (r * ln (g x) + m * f x / g x)"
-    using pos
-    by (auto intro!: derivative_eq_intros g pos f simp: powr_def field_simps exp_diff)
-  then show ?thesis
-  proof (rule DERIV_cong_ev[OF refl _ refl, THEN iffD1, rotated])
-    from DERIV_isCont[OF g] pos have "\<forall>\<^sub>F x in at x. 0 < g x"
-      unfolding isCont_def by (rule order_tendstoD(1))
-    with pos show "\<forall>\<^sub>F x in nhds x. exp (f x * ln (g x)) = g x powr f x"
-      by (auto simp: eventually_at_filter powr_def elim: eventually_mono)
-  qed
-qed
+  using assms
+  by (auto intro!: derivative_eq_intros ext simp: has_field_derivative_def algebra_simps)
 
 lemma DERIV_fun_powr:
   fixes r :: real
@@ -3344,6 +3357,8 @@
 declare DERIV_sin[THEN DERIV_chain2, derivative_intros]
   and DERIV_sin[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_sin[derivative_intros] = DERIV_sin[THEN DERIV_compose_FDERIV]
+
 lemma DERIV_cos [simp]: "DERIV cos x :> - sin x"
   for x :: "'a::{real_normed_field,banach}"
   unfolding sin_def cos_def scaleR_conv_of_real
@@ -3359,6 +3374,8 @@
 declare DERIV_cos[THEN DERIV_chain2, derivative_intros]
   and DERIV_cos[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_cos[derivative_intros] = DERIV_cos[THEN DERIV_compose_FDERIV]
+
 lemma isCont_sin: "isCont sin x"
   for x :: "'a::{real_normed_field,banach}"
   by (rule DERIV_sin [THEN DERIV_isCont])
@@ -4598,6 +4615,8 @@
   unfolding tan_def
   by (auto intro!: derivative_eq_intros, simp add: divide_inverse power2_eq_square)
 
+lemmas has_derivative_tan[derivative_intros] = DERIV_tan[THEN DERIV_compose_FDERIV]
+
 lemma isCont_tan: "cos x \<noteq> 0 \<Longrightarrow> isCont tan x"
   for x :: "'a::{real_normed_field,banach}"
   by (rule DERIV_tan [THEN DERIV_isCont])
@@ -5265,6 +5284,10 @@
   DERIV_arctan[THEN DERIV_chain2, derivative_intros]
   DERIV_arctan[THEN DERIV_chain2, unfolded has_field_derivative_def, derivative_intros]
 
+lemmas has_derivative_arctan[derivative_intros] = DERIV_arctan[THEN DERIV_compose_FDERIV]
+  and has_derivative_arccos[derivative_intros] = DERIV_arccos[THEN DERIV_compose_FDERIV]
+  and has_derivative_arcsin[derivative_intros] = DERIV_arcsin[THEN DERIV_compose_FDERIV]
+
 lemma filterlim_tan_at_right: "filterlim tan at_bot (at_right (- (pi/2)))"
   by (rule filterlim_at_bot_at_right[where Q="\<lambda>x. - pi/2 < x \<and> x < pi/2" and P="\<lambda>x. True" and g=arctan])
      (auto simp: arctan le_less eventually_at dist_real_def simp del: less_divide_eq_numeral1