# HG changeset patch
# User immler
# Date 1519626845 -3600
# Node ID ce3e87a514884bbc9f306034e0d160c39b53516d
# Parent  0cd2fd0c2dcfd49d1e3da7f87d985c13f000ed2e
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements

diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Analysis/Analysis.thy
--- a/src/HOL/Analysis/Analysis.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Analysis/Analysis.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -23,6 +23,7 @@
   Generalised_Binomial_Theorem
   Gamma_Function
   Ball_Volume
+  Lipschitz
 begin
 
 end
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Analysis/Connected.thy
--- a/src/HOL/Analysis/Connected.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Analysis/Connected.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -2727,6 +2727,13 @@
   using diameter_bounded_bound[of s] diameter_lower_bounded[of s] assms
   by auto
 
+lemma bounded_two_points:
+  "bounded S \<longleftrightarrow> (\<exists>e. \<forall>x\<in>S. \<forall>y\<in>S. dist x y \<le> e)"
+  apply (rule iffI)
+  subgoal using diameter_bounded(1) by auto
+  subgoal using bounded_any_center[of S] by meson
+  done
+
 lemma diameter_compact_attained:
   assumes "compact s"
     and "s \<noteq> {}"
@@ -3797,6 +3804,14 @@
   using assms homeomorphic_ball01_UNIV homeomorphic_balls(1) homeomorphic_trans zero_less_one by blast
 
 
+text \<open>Connectedness is invariant under homeomorphisms.\<close>
+
+lemma homeomorphic_connectedness:
+  assumes "s homeomorphic t"
+  shows "connected s \<longleftrightarrow> connected t"
+using assms unfolding homeomorphic_def homeomorphism_def by (metis connected_continuous_image)
+
+
 subsection\<open>Inverse function property for open/closed maps\<close>
 
 lemma continuous_on_inverse_open_map:
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Analysis/Extended_Real_Limits.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Analysis/Extended_Real_Limits.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -936,6 +936,18 @@
 
 subsubsection \<open>Further limits\<close>
 
+text \<open>The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\<close>
+
+lemma tendsto_diff_ereal_general [tendsto_intros]:
+  fixes u v::"'a \<Rightarrow> ereal"
+  assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>((l = \<infinity> \<and> m = \<infinity>) \<or> (l = -\<infinity> \<and> m = -\<infinity>))"
+  shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"
+proof -
+  have "((\<lambda>n. u n + (-v n)) \<longlongrightarrow> l + (-m)) F"
+    apply (intro tendsto_intros assms) using assms by (auto simp add: ereal_uminus_eq_reorder)
+  then show ?thesis by (simp add: minus_ereal_def)
+qed
+
 lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
   "(\<lambda> n::nat. real n) \<longlonglongrightarrow> \<infinity>"
 by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)
@@ -1091,6 +1103,62 @@
 qed(simp)
 
 
+lemma continuous_ereal_abs:
+  "continuous_on (UNIV::ereal set) abs"
+proof -
+  have "continuous_on ({..0} \<union> {(0::ereal)..}) abs"
+    apply (rule continuous_on_closed_Un, auto)
+    apply (rule iffD1[OF continuous_on_cong, of "{..0}" _ "\<lambda>x. -x"])
+    using less_eq_ereal_def apply (auto simp add: continuous_uminus_ereal)
+    apply (rule iffD1[OF continuous_on_cong, of "{0..}" _ "\<lambda>x. x"])
+      apply (auto simp add: continuous_on_id)
+    done
+  moreover have "(UNIV::ereal set) = {..0} \<union> {(0::ereal)..}" by auto
+  ultimately show ?thesis by auto
+qed
+
+lemmas continuous_on_compose_ereal_abs[continuous_intros] =
+  continuous_on_compose2[OF continuous_ereal_abs _ subset_UNIV]
+
+lemma tendsto_abs_ereal [tendsto_intros]:
+  assumes "(u \<longlongrightarrow> (l::ereal)) F"
+  shows "((\<lambda>n. abs(u n)) \<longlongrightarrow> abs l) F"
+using continuous_ereal_abs assms by (metis UNIV_I continuous_on tendsto_compose)
+
+lemma ereal_minus_real_tendsto_MInf [tendsto_intros]:
+  "(\<lambda>x. ereal (- real x)) \<longlonglongrightarrow> - \<infinity>"
+by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)
+
+
+subsection \<open>Extended-Nonnegative-Real.thy\<close>
+
+lemma tendsto_diff_ennreal_general [tendsto_intros]:
+  fixes u v::"'a \<Rightarrow> ennreal"
+  assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>(l = \<infinity> \<and> m = \<infinity>)"
+  shows "((\<lambda>n. u n - v n) \<longlongrightarrow> l - m) F"
+proof -
+  have "((\<lambda>n. e2ennreal(enn2ereal(u n) - enn2ereal(v n))) \<longlongrightarrow> e2ennreal(enn2ereal l - enn2ereal m)) F"
+    apply (intro tendsto_intros) using assms by  auto
+  then show ?thesis by auto
+qed
+
+lemma tendsto_mult_ennreal [tendsto_intros]:
+  fixes l m::ennreal
+  assumes "(u \<longlongrightarrow> l) F" "(v \<longlongrightarrow> m) F" "\<not>((l = 0 \<and> m = \<infinity>) \<or> (l = \<infinity> \<and> m = 0))"
+  shows "((\<lambda>n. u n * v n) \<longlongrightarrow> l * m) F"
+proof -
+  have "((\<lambda>n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \<longlongrightarrow> e2ennreal(enn2ereal l * enn2ereal m)) F"
+    apply (intro tendsto_intros) using assms apply auto
+    using enn2ereal_inject zero_ennreal.rep_eq by fastforce+
+  moreover have "e2ennreal(enn2ereal (u n) * enn2ereal (v n)) = u n * v n" for n
+    by (subst times_ennreal.abs_eq[symmetric], auto simp add: eq_onp_same_args)
+  moreover have "e2ennreal(enn2ereal l * enn2ereal m)  = l * m"
+    by (subst times_ennreal.abs_eq[symmetric], auto simp add: eq_onp_same_args)
+  ultimately show ?thesis
+    by auto
+qed
+
+
 subsection \<open>monoset\<close>
 
 definition (in order) mono_set:
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Analysis/Lipschitz.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Analysis/Lipschitz.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -0,0 +1,834 @@
+(*  Title:      HOL/Analysis/Lipschitz.thy
+    Author:     Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
+    Author:     Fabian Immler, TU München
+*)
+section \<open>Lipschitz continuity\<close>
+theory Lipschitz
+  imports Borel_Space
+begin
+
+definition lipschitz_on
+  where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))"
+
+bundle lipschitz_syntax begin
+notation lipschitz_on ("_-lipschitz'_on" [1000])
+end
+bundle no_lipschitz_syntax begin
+no_notation lipschitz_on ("_-lipschitz'_on" [1000])
+end
+
+unbundle lipschitz_syntax
+
+lemma lipschitz_onI: "L-lipschitz_on X f"
+  if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y" "0 \<le> L"
+  using that by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_onD:
+  "dist (f x) (f y) \<le> L * dist x y"
+  if "L-lipschitz_on X f" "x \<in> X" "y \<in> X"
+  using that by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_on_nonneg:
+  "0 \<le> L" if "L-lipschitz_on X f"
+  using that by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_on_normD:
+  "norm (f x - f y) \<le> L * norm (x - y)"
+  if "lipschitz_on L X f" "x \<in> X" "y \<in> X"
+  using lipschitz_onD[OF that]
+  by (simp add: dist_norm)
+
+lemma lipschitz_on_mono: "L-lipschitz_on D f" if "M-lipschitz_on E f" "D \<subseteq> E" "M \<le> L"
+  using that
+  by (force simp: lipschitz_on_def intro: order_trans[OF _ mult_right_mono])
+
+lemmas lipschitz_on_subset = lipschitz_on_mono[OF _ _ order_refl]
+  and lipschitz_on_le = lipschitz_on_mono[OF _ order_refl]
+
+lemma lipschitz_on_leI:
+  "L-lipschitz_on X f"
+  if "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> x \<le> y \<Longrightarrow> dist (f x) (f y) \<le> L * dist x y"
+    "0 \<le> L"
+  for f::"'a::{linorder_topology, ordered_real_vector, metric_space} \<Rightarrow> 'b::metric_space"
+proof (rule lipschitz_onI)
+  fix x y assume xy: "x \<in> X" "y \<in> X"
+  consider "y \<le> x" | "x \<le> y"
+    by (rule le_cases)
+  then show "dist (f x) (f y) \<le> L * dist x y"
+  proof cases
+    case 1
+    then have "dist (f y) (f x) \<le> L * dist y x"
+      by (auto intro!: that xy)
+    then show ?thesis
+      by (simp add: dist_commute)
+  qed (auto intro!: that xy)
+qed fact
+
+lemma lipschitz_on_concat:
+  fixes a b c::real
+  assumes f: "L-lipschitz_on {a .. b} f"
+  assumes g: "L-lipschitz_on {b .. c} g"
+  assumes fg: "f b = g b"
+  shows "lipschitz_on L {a .. c} (\<lambda>x. if x \<le> b then f x else g x)"
+    (is "lipschitz_on _ _ ?f")
+proof (rule lipschitz_on_leI)
+  fix x y
+  assume x: "x \<in> {a..c}" and y: "y \<in> {a..c}" and xy: "x \<le> y"
+  consider "x \<le> b \<and> b < y" | "x \<ge> b \<or> y \<le> b" by arith
+  then show "dist (?f x) (?f y) \<le> L * dist x y"
+  proof cases
+    case 1
+    have "dist (f x) (g y) \<le> dist (f x) (f b) + dist (g b) (g y)"
+      unfolding fg by (rule dist_triangle)
+    also have "dist (f x) (f b) \<le> L * dist x b"
+      using 1 x
+      by (auto intro!: lipschitz_onD[OF f])
+    also have "dist (g b) (g y) \<le> L * dist b y"
+      using 1 x y
+      by (auto intro!: lipschitz_onD[OF g] lipschitz_onD[OF f])
+    finally have "dist (f x) (g y) \<le> L * dist x b + L * dist b y"
+      by simp
+    also have "\<dots> = L * (dist x b + dist b y)"
+      by (simp add: algebra_simps)
+    also have "dist x b + dist b y = dist x y"
+      using 1 x y
+      by (auto simp: dist_real_def abs_real_def)
+    finally show ?thesis
+      using 1 by simp
+  next
+    case 2
+    with lipschitz_onD[OF f, of x y] lipschitz_onD[OF g, of x y] x y xy
+    show ?thesis
+      by (auto simp: fg)
+  qed
+qed (rule lipschitz_on_nonneg[OF f])
+
+proposition lipschitz_on_concat_max:
+  fixes a b c::real
+  assumes f: "L-lipschitz_on {a .. b} f"
+  assumes g: "M-lipschitz_on {b .. c} g"
+  assumes fg: "f b = g b"
+  shows "(max L M)-lipschitz_on {a .. c} (\<lambda>x. if x \<le> b then f x else g x)"
+proof -
+  have "lipschitz_on (max L M) {a .. b} f" "lipschitz_on (max L M) {b .. c} g"
+    by (auto intro!: lipschitz_on_mono[OF f order_refl] lipschitz_on_mono[OF g order_refl])
+  from lipschitz_on_concat[OF this fg] show ?thesis .
+qed
+
+
+subsubsection \<open>Continuity\<close>
+
+lemma lipschitz_on_uniformly_continuous:
+  assumes "L-lipschitz_on X f"
+  shows "uniformly_continuous_on X f"
+  unfolding uniformly_continuous_on_def
+proof safe
+  fix e::real
+  assume "0 < e"
+  from assms have l: "(L+1)-lipschitz_on X f"
+    by (rule lipschitz_on_mono) auto
+  show "\<exists>d>0. \<forall>x\<in>X. \<forall>x'\<in>X. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
+    using lipschitz_onD[OF l] lipschitz_on_nonneg[OF assms] \<open>0 < e\<close>
+    by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps)
+qed
+
+lemma lipschitz_on_continuous_on:
+  "continuous_on X f" if "L-lipschitz_on X f"
+  by (rule uniformly_continuous_imp_continuous[OF lipschitz_on_uniformly_continuous[OF that]])
+
+lemma lipschitz_on_continuous_within:
+  "continuous (at x within X) f" if "L-lipschitz_on X f" "x \<in> X"
+  using lipschitz_on_continuous_on[OF that(1)] that(2)
+  by (auto simp: continuous_on_eq_continuous_within)
+
+subsubsection \<open>Differentiable functions\<close>
+
+lemma bounded_derivative_imp_lipschitz:
+  assumes "\<And>x. x \<in> X \<Longrightarrow> (f has_derivative f' x) (at x within X)"
+  assumes convex: "convex X"
+  assumes "\<And>x. x \<in> X \<Longrightarrow> onorm (f' x) \<le> C" "0 \<le> C"
+  shows "C-lipschitz_on X f"
+proof (rule lipschitz_onI)
+  show "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> C * dist x y"
+    by (auto intro!: assms differentiable_bound[unfolded dist_norm[symmetric], OF convex])
+qed fact
+
+
+subsubsection \<open>Structural introduction rules\<close>
+
+named_theorems lipschitz_intros "structural introduction rules for Lipschitz controls"
+
+lemma lipschitz_on_compose [lipschitz_intros]:
+  "(D * C)-lipschitz_on U (g o f)"
+  if f: "C-lipschitz_on U f" and g: "D-lipschitz_on (f`U) g"
+proof (rule lipschitz_onI)
+  show "D* C \<ge> 0" using lipschitz_on_nonneg[OF f] lipschitz_on_nonneg[OF g] by auto
+  fix x y assume H: "x \<in> U" "y \<in> U"
+  have "dist (g (f x)) (g (f y)) \<le> D * dist (f x) (f y)"
+    apply (rule lipschitz_onD[OF g]) using H by auto
+  also have "... \<le> D * C * dist x y"
+    using mult_left_mono[OF lipschitz_onD(1)[OF f H] lipschitz_on_nonneg[OF g]] by auto
+  finally show "dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> D * C* dist x y"
+    unfolding comp_def by (auto simp add: mult.commute)
+qed
+
+lemma lipschitz_on_compose2:
+  "(D * C)-lipschitz_on U (\<lambda>x. g (f x))"
+  if "C-lipschitz_on U f" "D-lipschitz_on (f`U) g"
+  using lipschitz_on_compose[OF that] by (simp add: o_def)
+
+lemma lipschitz_on_cong[cong]:
+  "C-lipschitz_on U g \<longleftrightarrow> D-lipschitz_on V f"
+  if "C = D" "U = V" "\<And>x. x \<in> V \<Longrightarrow> g x = f x"
+  using that by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_on_transform:
+  "C-lipschitz_on U g"
+  if "C-lipschitz_on U f"
+    "\<And>x. x \<in> U \<Longrightarrow> g x = f x"
+  using that
+  by simp
+
+lemma lipschitz_on_empty_iff[simp]: "C-lipschitz_on {} f \<longleftrightarrow> C \<ge> 0"
+  by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_on_insert_iff[simp]:
+  "C-lipschitz_on (insert y X) f \<longleftrightarrow>
+    C-lipschitz_on X f \<and> (\<forall>x \<in> X. dist (f x) (f y) \<le> C * dist x y)"
+  by (auto simp: lipschitz_on_def dist_commute)
+
+lemma lipschitz_on_singleton [lipschitz_intros]: "C \<ge> 0 \<Longrightarrow> C-lipschitz_on {x} f"
+  and lipschitz_on_empty [lipschitz_intros]: "C \<ge> 0 \<Longrightarrow> C-lipschitz_on {} f"
+  by simp_all
+
+lemma lipschitz_on_id [lipschitz_intros]: "1-lipschitz_on U (\<lambda>x. x)"
+  by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_on_constant [lipschitz_intros]: "0-lipschitz_on U (\<lambda>x. c)"
+  by (auto simp: lipschitz_on_def)
+
+lemma lipschitz_on_add [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
+  assumes "C-lipschitz_on U f"
+    "D-lipschitz_on U g"
+  shows "(C+D)-lipschitz_on U (\<lambda>x. f x + g x)"
+proof (rule lipschitz_onI)
+  show "C + D \<ge> 0"
+    using lipschitz_on_nonneg[OF assms(1)] lipschitz_on_nonneg[OF assms(2)] by auto
+  fix x y assume H: "x \<in> U" "y \<in> U"
+  have "dist (f x + g x) (f y + g y) \<le> dist (f x) (f y) + dist (g x) (g y)"
+    by (simp add: dist_triangle_add)
+  also have "... \<le> C * dist x y + D * dist x y"
+    using lipschitz_onD(1)[OF assms(1) H] lipschitz_onD(1)[OF assms(2) H] by auto
+  finally show "dist (f x + g x) (f y + g y) \<le> (C+D) * dist x y" by (auto simp add: algebra_simps)
+qed
+
+lemma lipschitz_on_cmult [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "C-lipschitz_on U f"
+  shows "(abs(a) * C)-lipschitz_on U (\<lambda>x. a *\<^sub>R f x)"
+proof (rule lipschitz_onI)
+  show "abs(a) * C \<ge> 0" using lipschitz_on_nonneg[OF assms(1)] by auto
+  fix x y assume H: "x \<in> U" "y \<in> U"
+  have "dist (a *\<^sub>R f x) (a *\<^sub>R f y) = abs(a) * dist (f x) (f y)"
+    by (metis dist_norm norm_scaleR real_vector.scale_right_diff_distrib)
+  also have "... \<le> abs(a) * C * dist x y"
+    using lipschitz_onD(1)[OF assms(1) H] by (simp add: Groups.mult_ac(1) mult_left_mono)
+  finally show "dist (a *\<^sub>R f x) (a *\<^sub>R f y) \<le> \<bar>a\<bar> * C * dist x y" by auto
+qed
+
+lemma lipschitz_on_cmult_real [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow> real"
+  assumes "C-lipschitz_on U f"
+  shows "(abs(a) * C)-lipschitz_on U (\<lambda>x. a * f x)"
+  using lipschitz_on_cmult[OF assms] by auto
+
+lemma lipschitz_on_cmult_nonneg [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "C-lipschitz_on U f"
+    "a \<ge> 0"
+  shows "(a * C)-lipschitz_on U (\<lambda>x. a *\<^sub>R f x)"
+  using lipschitz_on_cmult[OF assms(1), of a] assms(2) by auto
+
+lemma lipschitz_on_cmult_real_nonneg [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow> real"
+  assumes "C-lipschitz_on U f"
+    "a \<ge> 0"
+  shows "(a * C)-lipschitz_on U (\<lambda>x. a * f x)"
+  using lipschitz_on_cmult_nonneg[OF assms] by auto
+
+lemma lipschitz_on_cmult_upper [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::real_normed_vector"
+  assumes "C-lipschitz_on U f"
+    "abs(a) \<le> D"
+  shows "(D * C)-lipschitz_on U (\<lambda>x. a *\<^sub>R f x)"
+  apply (rule lipschitz_on_mono[OF lipschitz_on_cmult[OF assms(1), of a], of _ "D * C"])
+  using assms(2) lipschitz_on_nonneg[OF assms(1)] mult_right_mono by auto
+
+lemma lipschitz_on_cmult_real_upper [lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow> real"
+  assumes "C-lipschitz_on U f"
+    "abs(a) \<le> D"
+  shows "(D * C)-lipschitz_on U (\<lambda>x. a * f x)"
+  using lipschitz_on_cmult_upper[OF assms] by auto
+
+lemma lipschitz_on_minus[lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
+  assumes "C-lipschitz_on U f"
+  shows "C-lipschitz_on U (\<lambda>x. - f x)"
+  by (metis (mono_tags, lifting) assms dist_minus lipschitz_on_def)
+
+lemma lipschitz_on_minus_iff[simp]:
+  "L-lipschitz_on X (\<lambda>x. - f x) \<longleftrightarrow> L-lipschitz_on X f"
+  "L-lipschitz_on X (- f) \<longleftrightarrow> L-lipschitz_on X f"
+  for f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
+  using lipschitz_on_minus[of L X f] lipschitz_on_minus[of L X "-f"]
+  by auto
+
+lemma lipschitz_on_diff[lipschitz_intros]:
+  fixes f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
+  assumes "C-lipschitz_on U f" "D-lipschitz_on U g"
+  shows "(C + D)-lipschitz_on U (\<lambda>x. f x - g x)"
+  using lipschitz_on_add[OF assms(1) lipschitz_on_minus[OF assms(2)]] by auto
+
+lemma lipschitz_on_closure [lipschitz_intros]:
+  assumes "C-lipschitz_on U f" "continuous_on (closure U) f"
+  shows "C-lipschitz_on (closure U) f"
+proof (rule lipschitz_onI)
+  show "C \<ge> 0" using lipschitz_on_nonneg[OF assms(1)] by simp
+  fix x y assume "x \<in> closure U" "y \<in> closure U"
+  obtain u v::"nat \<Rightarrow> 'a" where *: "\<And>n. u n \<in> U" "u \<longlonglongrightarrow> x"
+                                   "\<And>n. v n \<in> U" "v \<longlonglongrightarrow> y"
+    using \<open>x \<in> closure U\<close> \<open>y \<in> closure U\<close> unfolding closure_sequential by blast
+  have a: "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x"
+    using *(1) *(2) \<open>x \<in> closure U\<close> \<open>continuous_on (closure U) f\<close>
+    unfolding comp_def continuous_on_closure_sequentially[of U f] by auto
+  have b: "(\<lambda>n. f (v n)) \<longlonglongrightarrow> f y"
+    using *(3) *(4) \<open>y \<in> closure U\<close> \<open>continuous_on (closure U) f\<close>
+    unfolding comp_def continuous_on_closure_sequentially[of U f] by auto
+  have l: "(\<lambda>n. C * dist (u n) (v n) - dist (f (u n)) (f (v n))) \<longlonglongrightarrow> C * dist x y - dist (f x) (f y)"
+    by (intro tendsto_intros * a b)
+  have "C * dist (u n) (v n) - dist (f (u n)) (f (v n)) \<ge> 0" for n
+    using lipschitz_onD(1)[OF assms(1) \<open>u n \<in> U\<close> \<open>v n \<in> U\<close>] by simp
+  then have "C * dist x y - dist (f x) (f y) \<ge> 0" using LIMSEQ_le_const[OF l, of 0] by auto
+  then show "dist (f x) (f y) \<le> C * dist x y" by auto
+qed
+
+lemma lipschitz_on_Pair[lipschitz_intros]:
+  assumes f: "L-lipschitz_on A f"
+  assumes g: "M-lipschitz_on A g"
+  shows "(sqrt (L\<^sup>2 + M\<^sup>2))-lipschitz_on A (\<lambda>a. (f a, g a))"
+proof (rule lipschitz_onI, goal_cases)
+  case (1 x y)
+  have "dist (f x, g x) (f y, g y) = sqrt ((dist (f x) (f y))\<^sup>2 + (dist (g x) (g y))\<^sup>2)"
+    by (auto simp add: dist_Pair_Pair real_le_lsqrt)
+  also have "\<dots> \<le> sqrt ((L * dist x y)\<^sup>2 + (M * dist x y)\<^sup>2)"
+    by (auto intro!: real_sqrt_le_mono add_mono power_mono 1 lipschitz_onD f g)
+  also have "\<dots> \<le> sqrt (L\<^sup>2 + M\<^sup>2) * dist x y"
+    by (auto simp: power_mult_distrib ring_distribs[symmetric] real_sqrt_mult)
+  finally show ?case .
+qed simp
+
+lemma lipschitz_extend_closure:
+  fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
+  assumes "C-lipschitz_on U f"
+  shows "\<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)"
+proof -
+  obtain g where g: "\<And>x. x \<in> U \<Longrightarrow> g x = f x" "uniformly_continuous_on (closure U) g"
+    using uniformly_continuous_on_extension_on_closure[OF lipschitz_on_uniformly_continuous[OF assms]] by metis
+  have "C-lipschitz_on (closure U) g"
+    apply (rule lipschitz_on_closure, rule lipschitz_on_transform[OF assms])
+    using g uniformly_continuous_imp_continuous[OF g(2)] by auto
+  then show ?thesis using g(1) by auto
+qed
+
+lemma (in bounded_linear) lipschitz_boundE:
+  obtains B where "B-lipschitz_on A f"
+proof -
+  from nonneg_bounded
+  obtain B where B: "B \<ge> 0" "\<And>x. norm (f x) \<le> B * norm x"
+    by (auto simp: ac_simps)
+  have "B-lipschitz_on A f"
+    by (auto intro!: lipschitz_onI B simp: dist_norm diff[symmetric])
+  thus ?thesis ..
+qed
+
+
+subsection \<open>Local Lipschitz continuity\<close>
+
+text \<open>Given a function defined on a real interval, it is Lipschitz-continuous if and only if
+it is locally so, as proved in the following lemmas. It is useful especially for
+piecewise-defined functions: if each piece is Lipschitz, then so is the whole function.
+The same goes for functions defined on geodesic spaces, or more generally on geodesic subsets
+in a metric space (for instance convex subsets in a real vector space), and this follows readily
+from the real case, but we will not prove it explicitly.
+
+We give several variations around this statement. This is essentially a connectedness argument.\<close>
+
+lemma locally_lipschitz_imp_lispchitz_aux:
+  fixes f::"real \<Rightarrow> ('a::metric_space)"
+  assumes "a \<le> b"
+          "continuous_on {a..b} f"
+          "\<And>x. x \<in> {a..<b} \<Longrightarrow> \<exists>y \<in> {x<..b}. dist (f y) (f x) \<le> M * (y-x)"
+  shows "dist (f b) (f a) \<le> M * (b-a)"
+proof -
+  define A where "A = {x \<in> {a..b}. dist (f x) (f a) \<le> M * (x-a)}"
+  have *: "A = (\<lambda>x. M * (x-a) - dist (f x) (f a))-`{0..} \<inter> {a..b}"
+    unfolding A_def by auto
+  have "a \<in> A" unfolding A_def using \<open>a \<le> b\<close> by auto
+  then have "A \<noteq> {}" by auto
+  moreover have "bdd_above A" unfolding A_def by auto
+  moreover have "closed A" unfolding * by (rule closed_vimage_Int, auto intro!: continuous_intros assms)
+  ultimately have "Sup A \<in> A" by (rule closed_contains_Sup)
+  have "Sup A = b"
+  proof (rule ccontr)
+    assume "Sup A \<noteq> b"
+    define x where "x = Sup A"
+    have I: "dist (f x) (f a) \<le> M * (x-a)" using \<open>Sup A \<in> A\<close> x_def A_def by auto
+    have "x \<in> {a..<b}" unfolding x_def using \<open>Sup A \<in> A\<close> \<open>Sup A \<noteq> b\<close> A_def by auto
+    then obtain y where J: "y \<in> {x<..b}" "dist (f y) (f x) \<le> M * (y-x)" using assms(3) by blast
+    have "dist (f y) (f a) \<le> dist (f y) (f x) + dist (f x) (f a)" by (rule dist_triangle)
+    also have "... \<le> M * (y-x) + M * (x-a)" using I J(2) by auto
+    finally have "dist (f y) (f a) \<le> M * (y-a)" by (auto simp add: algebra_simps)
+    then have "y \<in> A" unfolding A_def using \<open>y \<in> {x<..b}\<close> \<open>x \<in> {a..<b}\<close> by auto
+    then have "y \<le> Sup A" by (rule cSup_upper, auto simp: A_def)
+    then show False using \<open>y \<in> {x<..b}\<close> x_def by auto
+  qed
+  then show ?thesis using \<open>Sup A \<in> A\<close> A_def by auto
+qed
+
+lemma locally_lipschitz_imp_lipschitz:
+  fixes f::"real \<Rightarrow> ('a::metric_space)"
+  assumes "continuous_on {a..b} f"
+          "\<And>x y. x \<in> {a..<b} \<Longrightarrow> y > x \<Longrightarrow> \<exists>z \<in> {x<..y}. dist (f z) (f x) \<le> M * (z-x)"
+          "M \<ge> 0"
+  shows "lipschitz_on M {a..b} f"
+proof (rule lipschitz_onI[OF _ \<open>M \<ge> 0\<close>])
+  have *: "dist (f t) (f s) \<le> M * (t-s)" if "s \<le> t" "s \<in> {a..b}" "t \<in> {a..b}" for s t
+  proof (rule locally_lipschitz_imp_lispchitz_aux, simp add: \<open>s \<le> t\<close>)
+    show "continuous_on {s..t} f" using continuous_on_subset[OF assms(1)] that by auto
+    fix x assume "x \<in> {s..<t}"
+    then have "x \<in> {a..<b}" using that by auto
+    show "\<exists>z\<in>{x<..t}. dist (f z) (f x) \<le> M * (z - x)"
+      using assms(2)[OF \<open>x \<in> {a..<b}\<close>, of t] \<open>x \<in> {s..<t}\<close> by auto
+  qed
+  fix x y assume "x \<in> {a..b}" "y \<in> {a..b}"
+  consider "x \<le> y" | "y \<le> x" by linarith
+  then show "dist (f x) (f y) \<le> M * dist x y"
+    apply (cases)
+    using *[OF _ \<open>x \<in> {a..b}\<close> \<open>y \<in> {a..b}\<close>] *[OF _ \<open>y \<in> {a..b}\<close> \<open>x \<in> {a..b}\<close>]
+    by (auto simp add: dist_commute dist_real_def)
+qed
+
+text \<open>We deduce that if a function is Lipschitz on finitely many closed sets on the real line, then
+it is Lipschitz on any interval contained in their union. The difficulty in the proof is to show
+that any point $z$ in this interval (except the maximum) has a point arbitrarily close to it on its
+right which is contained in a common initial closed set. Otherwise, we show that there is a small
+interval $(z, T)$ which does not intersect any of the initial closed sets, a contradiction.\<close>
+
+proposition lipschitz_on_closed_Union:
+  assumes "\<And>i. i \<in> I \<Longrightarrow> lipschitz_on M (U i) f"
+          "\<And>i. i \<in> I \<Longrightarrow> closed (U i)"
+          "finite I"
+          "M \<ge> 0"
+          "{u..(v::real)} \<subseteq> (\<Union>i\<in>I. U i)"
+  shows "lipschitz_on M {u..v} f"
+proof (rule locally_lipschitz_imp_lipschitz[OF _ _ \<open>M \<ge> 0\<close>])
+  have *: "continuous_on (U i) f" if "i \<in> I" for i
+    by (rule lipschitz_on_continuous_on[OF assms(1)[OF \<open>i\<in> I\<close>]])
+  have "continuous_on (\<Union>i\<in>I. U i) f"
+    apply (rule continuous_on_closed_Union) using \<open>finite I\<close> * assms(2) by auto
+  then show "continuous_on {u..v} f"
+    using \<open>{u..(v::real)} \<subseteq> (\<Union>i\<in>I. U i)\<close> continuous_on_subset by auto
+
+  fix z Z assume z: "z \<in> {u..<v}" "z < Z"
+  then have "u \<le> v" by auto
+  define T where "T = min Z v"
+  then have T: "T > z" "T \<le> v" "T \<ge> u" "T \<le> Z" using z by auto
+  define A where "A = (\<Union>i\<in> I \<inter> {i. U i \<inter> {z<..T} \<noteq> {}}. U i \<inter> {z..T})"
+  have a: "closed A"
+    unfolding A_def apply (rule closed_UN) using \<open>finite I\<close> \<open>\<And>i. i \<in> I \<Longrightarrow> closed (U i)\<close> by auto
+  have b: "bdd_below A" unfolding A_def using \<open>finite I\<close> by auto
+  have "\<exists>i \<in> I. T \<in> U i" using \<open>{u..v} \<subseteq> (\<Union>i\<in>I. U i)\<close> T by auto
+  then have c: "T \<in> A" unfolding A_def using T by (auto, fastforce)
+  have "Inf A \<ge> z"
+    apply (rule cInf_greatest, auto) using c unfolding A_def by auto
+  moreover have "Inf A \<le> z"
+  proof (rule ccontr)
+    assume "\<not>(Inf A \<le> z)"
+    then obtain w where w: "w > z" "w < Inf A" by (meson dense not_le_imp_less)
+    have "Inf A \<le> T" using a b c by (simp add: cInf_lower)
+    then have "w \<le> T" using w by auto
+    then have "w \<in> {u..v}" using w \<open>z \<in> {u..<v}\<close> T by auto
+    then obtain j where j: "j \<in> I" "w \<in> U j" using \<open>{u..v} \<subseteq> (\<Union>i\<in>I. U i)\<close> by fastforce
+    then have "w \<in> U j \<inter> {z..T}" "U j \<inter> {z<..T} \<noteq> {}" using j T w \<open>w \<le> T\<close> by auto
+    then have "w \<in> A" unfolding A_def using \<open>j \<in> I\<close> by auto
+    then have "Inf A \<le> w" using a b by (simp add: cInf_lower)
+    then show False using w by auto
+  qed
+  ultimately have "Inf A = z" by simp
+  moreover have "Inf A \<in> A"
+    apply (rule closed_contains_Inf) using a b c by auto
+  ultimately have "z \<in> A" by simp
+  then obtain i where i: "i \<in> I" "U i \<inter> {z<..T} \<noteq> {}" "z \<in> U i" unfolding A_def by auto
+  then obtain t where "t \<in> U i \<inter> {z<..T}" by blast
+  then have "dist (f t) (f z) \<le> M * (t - z)"
+    using lipschitz_onD(1)[OF assms(1)[of i], of t z] i dist_real_def by auto
+  then show "\<exists>t\<in>{z<..Z}. dist (f t) (f z) \<le> M * (t - z)" using \<open>T \<le> Z\<close> \<open>t \<in> U i \<inter> {z<..T}\<close> by auto
+qed
+
+
+subsection \<open>Local Lipschitz continuity (uniform for a family of functions)\<close>
+
+definition local_lipschitz::
+  "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c::metric_space) \<Rightarrow> bool"
+  where
+  "local_lipschitz T X f \<equiv> \<forall>x \<in> X. \<forall>t \<in> T.
+    \<exists>u>0. \<exists>L. \<forall>t \<in> cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
+
+lemma local_lipschitzI:
+  assumes "\<And>t x. t \<in> T \<Longrightarrow> x \<in> X \<Longrightarrow> \<exists>u>0. \<exists>L. \<forall>t \<in> cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
+  shows "local_lipschitz T X f"
+  using assms
+  unfolding local_lipschitz_def
+  by auto
+
+lemma local_lipschitzE:
+  assumes local_lipschitz: "local_lipschitz T X f"
+  assumes "t \<in> T" "x \<in> X"
+  obtains u L where "u > 0" "\<And>s. s \<in> cball t u \<inter> T \<Longrightarrow> L-lipschitz_on (cball x u \<inter> X) (f s)"
+  using assms local_lipschitz_def
+  by metis
+
+lemma local_lipschitz_continuous_on:
+  assumes local_lipschitz: "local_lipschitz T X f"
+  assumes "t \<in> T"
+  shows "continuous_on X (f t)"
+  unfolding continuous_on_def
+proof safe
+  fix x assume "x \<in> X"
+  from local_lipschitzE[OF local_lipschitz \<open>t \<in> T\<close> \<open>x \<in> X\<close>] obtain u L
+    where "0 < u"
+    and L: "\<And>s. s \<in> cball t u \<inter> T \<Longrightarrow> L-lipschitz_on (cball x u \<inter> X) (f s)"
+    by metis
+  have "x \<in> ball x u" using \<open>0 < u\<close> by simp
+  from lipschitz_on_continuous_on[OF L]
+  have tendsto: "(f t \<longlongrightarrow> f t x) (at x within cball x u \<inter> X)"
+    using \<open>0 < u\<close> \<open>x \<in> X\<close> \<open>t \<in> T\<close>
+    by (auto simp: continuous_on_def)
+  moreover have "\<forall>\<^sub>F xa in at x. (xa \<in> cball x u \<inter> X) = (xa \<in> X)"
+    using eventually_at_ball[OF \<open>0 < u\<close>, of x UNIV]
+    by eventually_elim auto
+  ultimately show "(f t \<longlongrightarrow> f t x) (at x within X)"
+    by (rule Lim_transform_within_set)
+qed
+
+lemma
+  local_lipschitz_compose1:
+  assumes ll: "local_lipschitz (g ` T) X (\<lambda>t. f t)"
+  assumes g: "continuous_on T g"
+  shows "local_lipschitz T X (\<lambda>t. f (g t))"
+proof (rule local_lipschitzI)
+  fix t x
+  assume "t \<in> T" "x \<in> X"
+  then have "g t \<in> g ` T" by simp
+  from local_lipschitzE[OF assms(1) this \<open>x \<in> X\<close>]
+  obtain u L where "0 < u" and l: "(\<And>s. s \<in> cball (g t) u \<inter> g ` T \<Longrightarrow> L-lipschitz_on (cball x u \<inter> X) (f s))"
+    by auto
+  from g[unfolded continuous_on_eq_continuous_within, rule_format, OF \<open>t \<in> T\<close>,
+    unfolded continuous_within_eps_delta, rule_format, OF \<open>0 < u\<close>]
+  obtain d where d: "d>0" "\<And>x'. x'\<in>T \<Longrightarrow> dist x' t < d \<Longrightarrow> dist (g x') (g t) < u"
+    by (auto)
+  show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on  (cball x u \<inter> X) (f (g t))"
+    using d \<open>0 < u\<close>
+    by (fastforce intro: exI[where x="(min d u)/2"] exI[where x=L]
+      intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute mem_ball mem_cball)
+qed
+
+context
+  fixes T::"'a::metric_space set" and X f
+  assumes local_lipschitz: "local_lipschitz T X f"
+begin
+
+lemma continuous_on_TimesI:
+  assumes y: "\<And>x. x \<in> X \<Longrightarrow> continuous_on T (\<lambda>t. f t x)"
+  shows "continuous_on (T \<times> X) (\<lambda>(t, x). f t x)"
+  unfolding continuous_on_iff
+proof (safe, simp)
+  fix a b and e::real
+  assume H: "a \<in> T" "b \<in> X" "0 < e"
+  hence "0 < e/2" by simp
+  from y[unfolded continuous_on_iff, OF \<open>b \<in> X\<close>, rule_format, OF \<open>a \<in> T\<close> \<open>0 < e/2\<close>]
+  obtain d where d: "d > 0" "\<And>t. t \<in> T \<Longrightarrow> dist t a < d \<Longrightarrow> dist (f t b) (f a b) < e/2"
+    by auto
+
+  from \<open>a : T\<close> \<open>b \<in> X\<close>
+  obtain u L where u: "0 < u"
+    and L: "\<And>t. t \<in> cball a u \<inter> T \<Longrightarrow> L-lipschitz_on  (cball b u \<inter> X) (f t)"
+    by (erule local_lipschitzE[OF local_lipschitz])
+
+  have "a \<in> cball a u \<inter> T" by (auto simp: \<open>0 < u\<close> \<open>a \<in> T\<close> less_imp_le)
+  from lipschitz_on_nonneg[OF L[OF \<open>a \<in> cball _ _ \<inter> _\<close>]] have "0 \<le> L" .
+
+  let ?d = "Min {d, u, (e/2/(L + 1))}"
+  show "\<exists>d>0. \<forall>x\<in>T. \<forall>y\<in>X. dist (x, y) (a, b) < d \<longrightarrow> dist (f x y) (f a b) < e"
+  proof (rule exI[where x = ?d], safe)
+    show "0 < ?d"
+      using \<open>0 \<le> L\<close> \<open>0 < u\<close> \<open>0 < e\<close> \<open>0 < d\<close>
+      by (auto intro!: divide_pos_pos )
+    fix x y
+    assume "x \<in> T" "y \<in> X"
+    assume dist_less: "dist (x, y) (a, b) < ?d"
+    have "dist y b \<le> dist (x, y) (a, b)"
+      using dist_snd_le[of "(x, y)" "(a, b)"]
+      by auto
+    also
+    note dist_less
+    also
+    {
+      note calculation
+      also have "?d \<le> u" by simp
+      finally have "dist y b < u" .
+    }
+    have "?d \<le> e/2/(L + 1)" by simp
+    also have "(L + 1) * \<dots> \<le> e / 2"
+      using \<open>0 < e\<close> \<open>L \<ge> 0\<close>
+      by (auto simp: divide_simps)
+    finally have le1: "(L + 1) * dist y b < e / 2" using \<open>L \<ge> 0\<close> by simp
+
+    have "dist x a \<le> dist (x, y) (a, b)"
+      using dist_fst_le[of "(x, y)" "(a, b)"]
+      by auto
+    also note dist_less
+    finally have "dist x a < ?d" .
+    also have "?d \<le> d" by simp
+    finally have "dist x a < d" .
+    note \<open>dist x a < ?d\<close>
+    also have "?d \<le> u" by simp
+    finally have "dist x a < u" .
+    then have "x \<in> cball a u \<inter> T"
+      using \<open>x \<in> T\<close>
+      by (auto simp: dist_commute mem_cball)
+    have "dist (f x y) (f a b) \<le> dist (f x y) (f x b) + dist (f x b) (f a b)"
+      by (rule dist_triangle)
+    also have "(L + 1)-lipschitz_on (cball b u \<inter> X) (f x)"
+      using L[OF \<open>x \<in> cball a u \<inter> T\<close>]
+      by (rule lipschitz_on_le) simp
+    then have "dist (f x y) (f x b) \<le> (L + 1) * dist y b"
+      apply (rule lipschitz_onD)
+      subgoal
+        using \<open>y \<in> X\<close> \<open>dist y b < u\<close>
+        by (simp add: dist_commute)
+      subgoal
+        using \<open>0 < u\<close> \<open>b \<in> X\<close>
+        by (simp add: )
+      done
+    also have "(L + 1) * dist y b \<le> e / 2"
+      using le1 \<open>0 \<le> L\<close> by simp
+    also have "dist (f x b) (f a b) < e / 2"
+      by (rule d; fact)
+    also have "e / 2 + e / 2 = e" by simp
+    finally show "dist (f x y) (f a b) < e" by simp
+  qed
+qed
+
+lemma local_lipschitz_compact_implies_lipschitz:
+  assumes "compact X" "compact T"
+  assumes cont: "\<And>x. x \<in> X \<Longrightarrow> continuous_on T (\<lambda>t. f t x)"
+  obtains L where "\<And>t. t \<in> T \<Longrightarrow> L-lipschitz_on X (f t)"
+proof -
+  {
+    assume *: "\<And>n::nat. \<not>(\<forall>t\<in>T. n-lipschitz_on X (f t))"
+    {
+      fix n::nat
+      from *[of n] have "\<exists>x y t. t \<in> T \<and> x \<in> X \<and> y \<in> X \<and> dist (f t y) (f t x) > n * dist y x"
+        by (force simp: lipschitz_on_def)
+    } then obtain t and x y::"nat \<Rightarrow> 'b" where xy: "\<And>n. x n \<in> X" "\<And>n. y n \<in> X"
+      and t: "\<And>n. t n \<in> T"
+      and d: "\<And>n. dist (f (t n) (y n)) (f (t n) (x n)) > n * dist (y n) (x n)"
+      by metis
+    from xy assms obtain lx rx where lx': "lx \<in> X" "strict_mono (rx :: nat \<Rightarrow> nat)" "(x o rx) \<longlonglongrightarrow> lx"
+      by (metis compact_def)
+    with xy have "\<And>n. (y o rx) n \<in> X" by auto
+    with assms obtain ly ry where ly': "ly \<in> X" "strict_mono (ry :: nat \<Rightarrow> nat)" "((y o rx) o ry) \<longlonglongrightarrow> ly"
+      by (metis compact_def)
+    with t have "\<And>n. ((t o rx) o ry) n \<in> T" by simp
+    with assms obtain lt rt where lt': "lt \<in> T" "strict_mono (rt :: nat \<Rightarrow> nat)" "(((t o rx) o ry) o rt) \<longlonglongrightarrow> lt"
+      by (metis compact_def)
+    from lx' ly'
+    have lx: "(x o (rx o ry o rt)) \<longlonglongrightarrow> lx" (is "?x \<longlonglongrightarrow> _")
+      and ly: "(y o (rx o ry o rt)) \<longlonglongrightarrow> ly" (is "?y \<longlonglongrightarrow> _")
+      and lt: "(t o (rx o ry o rt)) \<longlonglongrightarrow> lt" (is "?t \<longlonglongrightarrow> _")
+      subgoal by (simp add: LIMSEQ_subseq_LIMSEQ o_assoc lt'(2))
+      subgoal by (simp add: LIMSEQ_subseq_LIMSEQ ly'(3) o_assoc lt'(2))
+      subgoal by (simp add: o_assoc lt'(3))
+      done
+    hence "(\<lambda>n. dist (?y n) (?x n)) \<longlonglongrightarrow> dist ly lx"
+      by (metis tendsto_dist)
+    moreover
+    let ?S = "(\<lambda>(t, x). f t x) ` (T \<times> X)"
+    have "eventually (\<lambda>n::nat. n > 0) sequentially"
+      by (metis eventually_at_top_dense)
+    hence "eventually (\<lambda>n. norm (dist (?y n) (?x n)) \<le> norm (\<bar>diameter ?S\<bar> / n) * 1) sequentially"
+    proof eventually_elim
+      case (elim n)
+      have "0 < rx (ry (rt n))" using \<open>0 < n\<close>
+        by (metis dual_order.strict_trans1 lt'(2) lx'(2) ly'(2) seq_suble)
+      have compact: "compact ?S"
+        by (auto intro!: compact_continuous_image continuous_on_subset[OF continuous_on_TimesI]
+          compact_Times \<open>compact X\<close> \<open>compact T\<close> cont)
+      have "norm (dist (?y n) (?x n)) = dist (?y n) (?x n)" by simp
+      also
+      from this elim d[of "rx (ry (rt n))"]
+      have "\<dots> < dist (f (?t n) (?y n)) (f (?t n) (?x n)) / rx (ry (rt (n)))"
+        using lx'(2) ly'(2) lt'(2) \<open>0 < rx _\<close>
+        by (auto simp add: divide_simps algebra_simps strict_mono_def)
+      also have "\<dots> \<le> diameter ?S / n"
+        by (force intro!: \<open>0 < n\<close> strict_mono_def xy diameter_bounded_bound frac_le
+          compact_imp_bounded compact t
+          intro: le_trans[OF seq_suble[OF lt'(2)]]
+            le_trans[OF seq_suble[OF ly'(2)]]
+            le_trans[OF seq_suble[OF lx'(2)]])
+      also have "\<dots> \<le> abs (diameter ?S) / n"
+        by (auto intro!: divide_right_mono)
+      finally show ?case by simp
+    qed
+    with _ have "(\<lambda>n. dist (?y n) (?x n)) \<longlonglongrightarrow> 0"
+      by (rule tendsto_0_le)
+        (metis tendsto_divide_0[OF tendsto_const] filterlim_at_top_imp_at_infinity
+          filterlim_real_sequentially)
+    ultimately have "lx = ly"
+      using LIMSEQ_unique by fastforce
+    with assms lx' have "lx \<in> X" by auto
+    from \<open>lt \<in> T\<close> this obtain u L where L: "u > 0" "\<And>t. t \<in> cball lt u \<inter> T \<Longrightarrow> L-lipschitz_on (cball lx u \<inter> X) (f t)"
+      by (erule local_lipschitzE[OF local_lipschitz])
+    hence "L \<ge> 0" by (force intro!: lipschitz_on_nonneg \<open>lt \<in> T\<close>)
+
+    from L lt ly lx \<open>lx = ly\<close>
+    have
+      "eventually (\<lambda>n. ?t n \<in> ball lt u) sequentially"
+      "eventually (\<lambda>n. ?y n \<in> ball lx u) sequentially"
+      "eventually (\<lambda>n. ?x n \<in> ball lx u) sequentially"
+      by (auto simp: dist_commute Lim mem_ball)
+    moreover have "eventually (\<lambda>n. n > L) sequentially"
+      by (metis filterlim_at_top_dense filterlim_real_sequentially)
+    ultimately
+    have "eventually (\<lambda>_. False) sequentially"
+    proof eventually_elim
+      case (elim n)
+      hence "dist (f (?t n) (?y n)) (f (?t n) (?x n)) \<le> L * dist (?y n) (?x n)"
+        using assms xy t
+        unfolding dist_norm[symmetric]
+        by (intro lipschitz_onD[OF L(2)]) (auto simp: mem_ball mem_cball)
+      also have "\<dots> \<le> n * dist (?y n) (?x n)"
+        using elim by (intro mult_right_mono) auto
+      also have "\<dots> \<le> rx (ry (rt n)) * dist (?y n) (?x n)"
+        by (intro mult_right_mono[OF _ zero_le_dist])
+           (meson lt'(2) lx'(2) ly'(2) of_nat_le_iff order_trans seq_suble)
+      also have "\<dots> < dist (f (?t n) (?y n)) (f (?t n) (?x n))"
+        by (auto intro!: d)
+      finally show ?case by simp
+    qed
+    hence False
+      by simp
+  } then obtain L where "\<And>t. t \<in> T \<Longrightarrow> L-lipschitz_on X (f t)"
+    by metis
+  thus ?thesis ..
+qed
+
+lemma local_lipschitz_subset:
+  assumes "S \<subseteq> T" "Y \<subseteq> X"
+  shows "local_lipschitz S Y f"
+proof (rule local_lipschitzI)
+  fix t x assume "t \<in> S" "x \<in> Y"
+  then have "t \<in> T" "x \<in> X" using assms by auto
+  from local_lipschitzE[OF local_lipschitz, OF this]
+  obtain u L where u: "0 < u" and L: "\<And>s. s \<in> cball t u \<inter> T \<Longrightarrow> L-lipschitz_on (cball x u \<inter> X) (f s)"
+    by blast
+  show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> S. L-lipschitz_on (cball x u \<inter> Y) (f t)"
+    using assms
+    by (auto intro: exI[where x=u] exI[where x=L]
+        intro!: u lipschitz_on_subset[OF _ Int_mono[OF order_refl \<open>Y \<subseteq> X\<close>]] L)
+qed
+
+end
+
+lemma local_lipschitz_minus:
+  fixes f::"'a::metric_space \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
+  shows "local_lipschitz T X (\<lambda>t x. - f t x) = local_lipschitz T X f"
+  by (auto simp: local_lipschitz_def lipschitz_on_minus)
+
+lemma local_lipschitz_PairI:
+  assumes f: "local_lipschitz A B (\<lambda>a b. f a b)"
+  assumes g: "local_lipschitz A B (\<lambda>a b. g a b)"
+  shows "local_lipschitz A B (\<lambda>a b. (f a b, g a b))"
+proof (rule local_lipschitzI)
+  fix t x assume "t \<in> A" "x \<in> B"
+  from local_lipschitzE[OF f this] local_lipschitzE[OF g this]
+  obtain u L v M where "0 < u" "(\<And>s. s \<in> cball t u \<inter> A \<Longrightarrow> L-lipschitz_on (cball x u \<inter> B) (f s))"
+    "0 < v" "(\<And>s. s \<in> cball t v \<inter> A \<Longrightarrow> M-lipschitz_on (cball x v \<inter> B) (g s))"
+    by metis
+  then show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> A. L-lipschitz_on (cball x u \<inter> B) (\<lambda>b. (f t b, g t b))"
+    by (intro exI[where x="min u v"])
+      (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair simp: mem_cball)
+qed
+
+lemma local_lipschitz_constI: "local_lipschitz S T (\<lambda>t x. f t)"
+  by (auto simp: intro!: local_lipschitzI lipschitz_on_constant intro: exI[where x=1])
+
+lemma (in bounded_linear) local_lipschitzI:
+  shows "local_lipschitz A B (\<lambda>_. f)"
+proof (rule local_lipschitzI, goal_cases)
+  case (1 t x)
+  from lipschitz_boundE[of "(cball x 1 \<inter> B)"] obtain C where "C-lipschitz_on (cball x 1 \<inter> B) f" by auto
+  then show ?case
+    by (auto intro: exI[where x=1])
+qed
+
+lemma c1_implies_local_lipschitz:
+  fixes T::"real set" and X::"'a::{banach,heine_borel} set"
+    and f::"real \<Rightarrow> 'a \<Rightarrow> 'a"
+  assumes f': "\<And>t x. t \<in> T \<Longrightarrow> x \<in> X \<Longrightarrow> (f t has_derivative blinfun_apply (f' (t, x))) (at x)"
+  assumes cont_f': "continuous_on (T \<times> X) f'"
+  assumes "open T"
+  assumes "open X"
+  shows "local_lipschitz T X f"
+proof (rule local_lipschitzI)
+  fix t x
+  assume "t \<in> T" "x \<in> X"
+  from open_contains_cball[THEN iffD1, OF \<open>open X\<close>, rule_format, OF \<open>x \<in> X\<close>]
+  obtain u where u: "u > 0" "cball x u \<subseteq> X" by auto
+  moreover
+  from open_contains_cball[THEN iffD1, OF \<open>open T\<close>, rule_format, OF \<open>t \<in> T\<close>]
+  obtain v where v: "v > 0" "cball t v \<subseteq> T" by auto
+  ultimately
+  have "compact (cball t v \<times> cball x u)" "cball t v \<times> cball x u \<subseteq> T \<times> X"
+    by (auto intro!: compact_Times)
+  then have "compact (f' ` (cball t v \<times> cball x u))"
+    by (auto intro!: compact_continuous_image continuous_on_subset[OF cont_f'])
+  then obtain B where B: "B > 0" "\<And>s y. s \<in> cball t v \<Longrightarrow> y \<in> cball x u \<Longrightarrow> norm (f' (s, y)) \<le> B"
+    by (auto dest!: compact_imp_bounded simp: bounded_pos simp: mem_ball)
+
+  have lipschitz: "B-lipschitz_on (cball x (min u v) \<inter> X) (f s)" if s: "s \<in> cball t v" for s
+  proof -
+    note s
+    also note \<open>cball t v \<subseteq> T\<close>
+    finally
+    have deriv: "\<forall>y\<in>cball x u. (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
+      using \<open>_ \<subseteq> X\<close>
+      by (auto intro!: has_derivative_at_within[OF f'])
+    have "norm (f s y - f s z) \<le> B * norm (y - z)"
+      if "y \<in> cball x u" "z \<in> cball x u"
+      for y z
+      using s that
+      by (intro differentiable_bound[OF convex_cball deriv])
+        (auto intro!: B  simp: norm_blinfun.rep_eq[symmetric] mem_cball)
+    then show ?thesis
+      using \<open>0 < B\<close>
+      by (auto intro!: lipschitz_onI simp: dist_norm mem_cball)
+  qed
+  show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
+    by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v mem_cball)
+qed
+
+end
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Analysis/Topology_Euclidean_Space.thy
--- a/src/HOL/Analysis/Topology_Euclidean_Space.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Analysis/Topology_Euclidean_Space.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -2527,6 +2527,14 @@
     \<Longrightarrow> connected S \<longleftrightarrow> (\<nexists>A B. closed A \<and> closed B \<and> A \<noteq> {} \<and> B \<noteq> {} \<and> A \<union> B = S \<and> A \<inter> B = {})"
   unfolding connected_closedin_eq closedin_closed_eq connected_closedin_eq by blast
 
+text \<open>If a connnected set is written as the union of two nonempty closed sets, then these sets
+have to intersect.\<close>
+
+lemma connected_as_closed_union:
+  assumes "connected C" "C = A \<union> B" "closed A" "closed B" "A \<noteq> {}" "B \<noteq> {}"
+  shows "A \<inter> B \<noteq> {}"
+by (metis assms closed_Un connected_closed_set)
+
 lemma closedin_subset_trans:
   "closedin (subtopology euclidean U) S \<Longrightarrow> S \<subseteq> T \<Longrightarrow> T \<subseteq> U \<Longrightarrow>
     closedin (subtopology euclidean T) S"
@@ -3285,6 +3293,11 @@
   unfolding closure_approachable
   using dense by force
 
+lemma closure_approachableD:
+  assumes "x \<in> closure S" "e>0"
+  shows "\<exists>y\<in>S. dist x y < e"
+  using assms unfolding closure_approachable by (auto simp add: dist_commute)
+
 lemma closed_approachable:
   fixes S :: "'a::metric_space set"
   shows "closed S \<Longrightarrow> (\<forall>e>0. \<exists>y\<in>S. dist y x < e) \<longleftrightarrow> x \<in> S"
@@ -5249,38 +5262,48 @@
 
 text \<open>Characterization of various kinds of continuity in terms of sequences.\<close>
 
+lemma continuous_within_sequentiallyI:
+  fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
+  assumes "\<And>u::nat \<Rightarrow> 'a. u \<longlonglongrightarrow> a \<Longrightarrow> (\<forall>n. u n \<in> s) \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f a"
+  shows "continuous (at a within s) f"
+  using assms unfolding continuous_within tendsto_def[where l = "f a"]
+  by (auto intro!: sequentially_imp_eventually_within)
+
+lemma continuous_within_tendsto_compose:
+  fixes f::"'a::t2_space \<Rightarrow> 'b::topological_space"
+  assumes "continuous (at a within s) f"
+          "eventually (\<lambda>n. x n \<in> s) F"
+          "(x \<longlongrightarrow> a) F "
+  shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
+proof -
+  have *: "filterlim x (inf (nhds a) (principal s)) F"
+    using assms(2) assms(3) unfolding at_within_def filterlim_inf by (auto simp add: filterlim_principal eventually_mono)
+  show ?thesis
+    by (auto simp add: assms(1) continuous_within[symmetric] tendsto_at_within_iff_tendsto_nhds[symmetric] intro!: filterlim_compose[OF _ *])
+qed
+
+lemma continuous_within_tendsto_compose':
+  fixes f::"'a::t2_space \<Rightarrow> 'b::topological_space"
+  assumes "continuous (at a within s) f"
+    "\<And>n. x n \<in> s"
+    "(x \<longlongrightarrow> a) F "
+  shows "((\<lambda>n. f (x n)) \<longlongrightarrow> f a) F"
+  by (auto intro!: continuous_within_tendsto_compose[OF assms(1)] simp add: assms)
+
 lemma continuous_within_sequentially:
-  fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
+  fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
   shows "continuous (at a within s) f \<longleftrightarrow>
     (\<forall>x. (\<forall>n::nat. x n \<in> s) \<and> (x \<longlongrightarrow> a) sequentially
          \<longrightarrow> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
-  (is "?lhs = ?rhs")
-proof
-  assume ?lhs
-  {
-    fix x :: "nat \<Rightarrow> 'a"
-    assume x: "\<forall>n. x n \<in> s" "\<forall>e>0. eventually (\<lambda>n. dist (x n) a < e) sequentially"
-    fix T :: "'b set"
-    assume "open T" and "f a \<in> T"
-    with \<open>?lhs\<close> obtain d where "d>0" and d:"\<forall>x\<in>s. 0 < dist x a \<and> dist x a < d \<longrightarrow> f x \<in> T"
-      unfolding continuous_within tendsto_def eventually_at by auto
-    have "eventually (\<lambda>n. dist (x n) a < d) sequentially"
-      using x(2) \<open>d>0\<close> by simp
-    then have "eventually (\<lambda>n. (f \<circ> x) n \<in> T) sequentially"
-    proof eventually_elim
-      case (elim n)
-      then show ?case
-        using d x(1) \<open>f a \<in> T\<close> by auto
-    qed
-  }
-  then show ?rhs
-    unfolding tendsto_iff tendsto_def by simp
-next
-  assume ?rhs
-  then show ?lhs
-    unfolding continuous_within tendsto_def [where l="f a"]
-    by (simp add: sequentially_imp_eventually_within)
-qed
+  using continuous_within_tendsto_compose'[of a s f _ sequentially]
+    continuous_within_sequentiallyI[of a s f]
+  by (auto simp: o_def)
+
+lemma continuous_at_sequentiallyI:
+  fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
+  assumes "\<And>u. u \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f a"
+  shows "continuous (at a) f"
+  using continuous_within_sequentiallyI[of a UNIV f] assms by auto
 
 lemma continuous_at_sequentially:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
@@ -5288,12 +5311,19 @@
     (\<forall>x. (x \<longlongrightarrow> a) sequentially --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
   using continuous_within_sequentially[of a UNIV f] by simp
 
+lemma continuous_on_sequentiallyI:
+  fixes f :: "'a::{first_countable_topology, t2_space} \<Rightarrow> 'b::topological_space"
+  assumes "\<And>u a. (\<forall>n. u n \<in> s) \<Longrightarrow> a \<in> s \<Longrightarrow> u \<longlonglongrightarrow> a \<Longrightarrow> (\<lambda>n. f (u n)) \<longlonglongrightarrow> f a"
+  shows "continuous_on s f"
+  using assms unfolding continuous_on_eq_continuous_within
+  using continuous_within_sequentiallyI[of _ s f] by auto
+
 lemma continuous_on_sequentially:
   fixes f :: "'a::metric_space \<Rightarrow> 'b::topological_space"
   shows "continuous_on s f \<longleftrightarrow>
     (\<forall>x. \<forall>a \<in> s. (\<forall>n. x(n) \<in> s) \<and> (x \<longlongrightarrow> a) sequentially
       --> ((f \<circ> x) \<longlongrightarrow> f a) sequentially)"
-  (is "?lhs = ?rhs")
+    (is "?lhs = ?rhs")
 proof
   assume ?rhs
   then show ?lhs
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Lattices.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -757,6 +757,11 @@
 
 end
 
+lemma max_of_antimono: "antimono f \<Longrightarrow> max (f x) (f y) = f (min x y)"
+  and min_of_antimono: "antimono f \<Longrightarrow> min (f x) (f y) = f (max x y)"
+  for f::"'a::linorder \<Rightarrow> 'b::linorder"
+  by (auto simp: antimono_def Orderings.max_def min_def intro!: antisym)
+
 lemma inf_min: "inf = (min :: 'a::{semilattice_inf,linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
   by (auto intro: antisym simp add: min_def fun_eq_iff)
 
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Library/Extended_Nonnegative_Real.thy
--- a/src/HOL/Library/Extended_Nonnegative_Real.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Library/Extended_Nonnegative_Real.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -1547,11 +1547,32 @@
   by (rule continuous_on_tendsto_compose[where g=f, OF ennreal_continuous_on_cmult, where s=UNIV])
      (auto simp: continuous_on_id)
 
-lemma tendsto_ennrealI[intro, simp]:
+lemma tendsto_ennrealI[intro, simp, tendsto_intros]:
   "(f \<longlongrightarrow> x) F \<Longrightarrow> ((\<lambda>x. ennreal (f x)) \<longlongrightarrow> ennreal x) F"
   by (auto simp: ennreal_def
            intro!: continuous_on_tendsto_compose[OF continuous_on_e2ennreal[of UNIV]] tendsto_max)
 
+lemma tendsto_enn2erealI [tendsto_intros]:
+  assumes "(f \<longlongrightarrow> l) F"
+  shows "((\<lambda>i. enn2ereal(f i)) \<longlongrightarrow> enn2ereal l) F"
+using tendsto_enn2ereal_iff assms by auto
+
+lemma tendsto_e2ennrealI [tendsto_intros]:
+  assumes "(f \<longlongrightarrow> l) F"
+  shows "((\<lambda>i. e2ennreal(f i)) \<longlongrightarrow> e2ennreal l) F"
+proof -
+  have *: "e2ennreal (max x 0) = e2ennreal x" for x
+    by (simp add: e2ennreal_def max.commute)
+  have "((\<lambda>i. max (f i) 0) \<longlongrightarrow> max l 0) F"
+    apply (intro tendsto_intros) using assms by auto
+  then have "((\<lambda>i. enn2ereal(e2ennreal (max (f i) 0))) \<longlongrightarrow> enn2ereal (e2ennreal (max l 0))) F"
+    by (subst enn2ereal_e2ennreal, auto)+
+  then have "((\<lambda>i. e2ennreal (max (f i) 0)) \<longlongrightarrow> e2ennreal (max l 0)) F"
+    using tendsto_enn2ereal_iff by auto
+  then show ?thesis
+    unfolding * by auto
+qed
+
 lemma ennreal_suminf_minus:
   fixes f g :: "nat \<Rightarrow> ennreal"
   shows "(\<And>i. g i \<le> f i) \<Longrightarrow> suminf f \<noteq> top \<Longrightarrow> suminf g \<noteq> top \<Longrightarrow> (\<Sum>i. f i - g i) = suminf f - suminf g"
@@ -1914,6 +1935,18 @@
   shows "a - b = a - c \<longleftrightarrow> (b = c \<or> (a \<le> b \<and> a \<le> c) \<or> a = top)"
   by (cases a; cases b; cases c) (auto simp: ennreal_minus_if)
 
+text \<open>The next lemma is wrong for $a = top$, for $b = c = 1$ for instance.\<close>
+
+lemma ennreal_right_diff_distrib:
+  fixes a b c::ennreal
+  assumes "a \<noteq> top"
+  shows "a * (b - c) = a * b - a * c"
+  apply (cases a, cases b, cases c, auto simp add: assms)
+  apply (metis (mono_tags, lifting) ennreal_minus ennreal_mult' linordered_field_class.sign_simps(38) split_mult_pos_le)
+  apply (metis ennreal_minus_zero ennreal_mult_cancel_left ennreal_top_eq_mult_iff minus_top_ennreal mult_eq_0_iff top_neq_ennreal)
+  apply (metis ennreal_minus_eq_top ennreal_minus_zero ennreal_mult_eq_top_iff mult_eq_0_iff)
+  done
+
 lemma SUP_diff_ennreal:
   "c < top \<Longrightarrow> (SUP i:I. f i - c :: ennreal) = (SUP i:I. f i) - c"
   by (auto intro!: SUP_eqI ennreal_minus_mono SUP_least intro: SUP_upper
@@ -1950,14 +1983,7 @@
 lemma enn2real_eq_0_iff: "enn2real x = 0 \<longleftrightarrow> x = 0 \<or> x = top"
   by (cases x) auto
 
-lemma (in -) continuous_on_diff_ereal:
-  "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>g x\<bar> \<noteq> \<infinity>) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ereal)"
-  apply (auto simp: continuous_on_def)
-  apply (intro tendsto_diff_ereal)
-  apply metis+
-  done
-
-lemma (in -) continuous_on_diff_ennreal:
+lemma continuous_on_diff_ennreal:
   "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> f x \<noteq> top) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> g x \<noteq> top) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ennreal)"
   including ennreal.lifting
 proof (transfer fixing: A, simp add: top_ereal_def)
@@ -1967,10 +1993,20 @@
     by (intro continuous_on_max continuous_on_const continuous_on_diff_ereal) auto
 qed
 
-lemma (in -) tendsto_diff_ennreal:
+lemma tendsto_diff_ennreal:
   "(f \<longlongrightarrow> x) F \<Longrightarrow> (g \<longlongrightarrow> y) F \<Longrightarrow> x \<noteq> top \<Longrightarrow> y \<noteq> top \<Longrightarrow> ((\<lambda>z. f z - g z::ennreal) \<longlongrightarrow> x - y) F"
   using continuous_on_tendsto_compose[where f="\<lambda>x. fst x - snd x::ennreal" and s="{(x, y). x \<noteq> top \<and> y \<noteq> top}" and g="\<lambda>x. (f x, g x)" and l="(x, y)" and F="F",
     OF continuous_on_diff_ennreal]
   by (auto simp: tendsto_Pair eventually_conj_iff less_top order_tendstoD continuous_on_fst continuous_on_snd continuous_on_id)
 
+declare lim_real_of_ereal [tendsto_intros]
+
+lemma tendsto_enn2real [tendsto_intros]:
+  assumes "(u \<longlongrightarrow> ennreal l) F" "l \<ge> 0"
+  shows "((\<lambda>n. enn2real (u n)) \<longlongrightarrow> l) F"
+  unfolding enn2real_def
+  apply (intro tendsto_intros)
+  apply (subst enn2ereal_ennreal[symmetric])
+  by (intro tendsto_intros assms)+
+
 end
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Library/Extended_Real.thy
--- a/src/HOL/Library/Extended_Real.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Library/Extended_Real.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -4297,6 +4297,14 @@
     by (simp add: x' y' cong: filterlim_cong)
 qed
 
+lemma continuous_on_diff_ereal:
+  "continuous_on A f \<Longrightarrow> continuous_on A g \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>) \<Longrightarrow> (\<And>x. x \<in> A \<Longrightarrow> \<bar>g x\<bar> \<noteq> \<infinity>) \<Longrightarrow> continuous_on A (\<lambda>z. f z - g z::ereal)"
+  apply (auto simp: continuous_on_def)
+  apply (intro tendsto_diff_ereal)
+  apply metis+
+  done
+
+
 subsubsection \<open>Tests for code generator\<close>
 
 text \<open>A small list of simple arithmetic expressions.\<close>
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Real_Vector_Spaces.thy
--- a/src/HOL/Real_Vector_Spaces.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Real_Vector_Spaces.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -1751,6 +1751,10 @@
 lemma (in metric_space) tendsto_iff: "(f \<longlongrightarrow> l) F \<longleftrightarrow> (\<forall>e>0. eventually (\<lambda>x. dist (f x) l < e) F)"
   unfolding nhds_metric filterlim_INF filterlim_principal by auto
 
+lemma tendsto_dist_iff:
+  "((f \<longlongrightarrow> l) F) \<longleftrightarrow> (((\<lambda>x. dist (f x) l) \<longlongrightarrow> 0) F)"
+  unfolding tendsto_iff by simp
+
 lemma (in metric_space) tendstoI [intro?]:
   "(\<And>e. 0 < e \<Longrightarrow> eventually (\<lambda>x. dist (f x) l < e) F) \<Longrightarrow> (f \<longlongrightarrow> l) F"
   by (auto simp: tendsto_iff)
@@ -2168,6 +2172,40 @@
   for X :: "nat \<Rightarrow> 'a::complete_space"
   by (blast intro: Cauchy_convergent convergent_Cauchy)
 
+text \<open>To prove that a Cauchy sequence converges, it suffices to show that a subsequence converges.\<close>
+
+lemma Cauchy_converges_subseq:
+  fixes u::"nat \<Rightarrow> 'a::metric_space"
+  assumes "Cauchy u"
+    "strict_mono r"
+    "(u o r) \<longlonglongrightarrow> l"
+  shows "u \<longlonglongrightarrow> l"
+proof -
+  have *: "eventually (\<lambda>n. dist (u n) l < e) sequentially" if "e > 0" for e
+  proof -
+    have "e/2 > 0" using that by auto
+    then obtain N1 where N1: "\<And>m n. m \<ge> N1 \<Longrightarrow> n \<ge> N1 \<Longrightarrow> dist (u m) (u n) < e/2"
+      using \<open>Cauchy u\<close> unfolding Cauchy_def by blast
+    obtain N2 where N2: "\<And>n. n \<ge> N2 \<Longrightarrow> dist ((u o r) n) l < e / 2"
+      using order_tendstoD(2)[OF iffD1[OF tendsto_dist_iff \<open>(u o r) \<longlonglongrightarrow> l\<close>] \<open>e/2 > 0\<close>]
+      unfolding eventually_sequentially by auto
+    have "dist (u n) l < e" if "n \<ge> max N1 N2" for n
+    proof -
+      have "dist (u n) l \<le> dist (u n) ((u o r) n) + dist ((u o r) n) l"
+        by (rule dist_triangle)
+      also have "... < e/2 + e/2"
+        apply (intro add_strict_mono)
+        using N1[of n "r n"] N2[of n] that unfolding comp_def
+        by (auto simp add: less_imp_le) (meson assms(2) less_imp_le order.trans seq_suble)
+      finally show ?thesis by simp
+    qed 
+    then show ?thesis unfolding eventually_sequentially by blast
+  qed
+  have "(\<lambda>n. dist (u n) l) \<longlonglongrightarrow> 0"
+    apply (rule order_tendstoI)
+    using * by auto (meson eventually_sequentiallyI less_le_trans zero_le_dist)
+  then show ?thesis using tendsto_dist_iff by auto
+qed
 
 subsection \<open>The set of real numbers is a complete metric space\<close>
 
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -1013,7 +1013,7 @@
   finally show ?thesis by simp
 qed
 
-lemma image_minus_const_greaterThanAtMost_real[simp]:
+lemma image_minus_const_greaterThanAtMost[simp]:
   fixes a b c::"'a::linordered_idom"
   shows "(-) c ` {a<..b} = {c - b..<c - a}"
 proof -
@@ -1023,7 +1023,7 @@
   finally show ?thesis by simp
 qed
 
-lemma image_minus_const_atLeast_real[simp]:
+lemma image_minus_const_atLeast[simp]:
   fixes a c::"'a::linordered_idom"
   shows "(-) c ` {a..} = {..c - a}"
 proof -
@@ -1033,7 +1033,7 @@
   finally show ?thesis by simp
 qed
 
-lemma image_minus_const_AtMost_real[simp]:
+lemma image_minus_const_AtMost[simp]:
   fixes b c::"'a::linordered_idom"
   shows "(-) c ` {..b} = {c - b..}"
 proof -
@@ -1043,6 +1043,10 @@
   finally show ?thesis by simp
 qed
 
+lemma image_minus_const_atLeastAtMost' [simp]:
+  "(\<lambda>t. t-d)`{a..b} = {a-d..b-d}" for d::"'a::linordered_idom"
+  by (metis (no_types, lifting) diff_conv_add_uminus image_add_atLeastAtMost' image_cong)
+
 context linordered_field begin
 
 lemma image_mult_atLeastAtMost [simp]:
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Topological_Spaces.thy
--- a/src/HOL/Topological_Spaces.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Topological_Spaces.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -1289,6 +1289,9 @@
 lemma strict_mono_o: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (r \<circ> s)"
   unfolding strict_mono_def by simp
 
+lemma strict_mono_compose: "strict_mono r \<Longrightarrow> strict_mono s \<Longrightarrow> strict_mono (\<lambda>x. r (s x))"
+  using strict_mono_o[of r s] by (simp add: o_def)
+
 lemma incseq_imp_monoseq:  "incseq X \<Longrightarrow> monoseq X"
   by (simp add: incseq_def monoseq_def)
 
@@ -1884,6 +1887,14 @@
   "closed s \<Longrightarrow> closed t \<Longrightarrow> continuous_on s f \<Longrightarrow> continuous_on t f \<Longrightarrow> continuous_on (s \<union> t) f"
   by (auto simp add: continuous_on_closed_vimage closed_Un Int_Un_distrib)
 
+lemma continuous_on_closed_Union:
+  assumes "finite I"
+    "\<And>i. i \<in> I \<Longrightarrow> closed (U i)"
+    "\<And>i. i \<in> I \<Longrightarrow> continuous_on (U i) f"
+  shows "continuous_on (\<Union> i \<in> I. U i) f"
+  using assms
+  by (induction I) (auto intro!: continuous_on_closed_Un)
+
 lemma continuous_on_If:
   assumes closed: "closed s" "closed t"
     and cont: "continuous_on s f" "continuous_on t g"
diff -r 0cd2fd0c2dcf -r ce3e87a51488 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Sun Feb 25 20:05:05 2018 +0100
+++ b/src/HOL/Transcendental.thy	Mon Feb 26 07:34:05 2018 +0100
@@ -2910,13 +2910,8 @@
 lemma log_base_root: "n > 0 \<Longrightarrow> b > 0 \<Longrightarrow> log (root n b) x = n * (log b x)"
   by (simp add: log_def ln_root)
 
-lemma ln_bound: "1 \<le> x \<Longrightarrow> ln x \<le> x"
-  for x :: real
-  apply (subgoal_tac "ln (1 + (x - 1)) \<le> x - 1")
-   apply simp
-  apply (rule ln_add_one_self_le_self)
-  apply simp
-  done
+lemma ln_bound: "0 < x \<Longrightarrow> ln x \<le> x" for x :: real
+  using ln_le_minus_one by force
 
 lemma powr_mono: "a \<le> b \<Longrightarrow> 1 \<le> x \<Longrightarrow> x powr a \<le> x powr b"
   for x :: real