moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
--- 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
--- 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:
--- 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:
--- /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
--- 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
--- 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)
--- 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
--- 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>
--- 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>
--- 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]:
--- 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"
--- 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