--- /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