src/HOL/Analysis/Lipschitz.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69566 c41954ee87cf
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     1 (*  Title:      HOL/Analysis/Lipschitz.thy
     2     Author:     Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
     3     Author:     Fabian Immler, TU München
     4 *)
     5 section \<open>Lipschitz Continuity\<close>
     6 
     7 theory Lipschitz
     8 imports Borel_Space
     9 begin
    10 
    11 definition%important lipschitz_on
    12   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))"
    13 
    14 bundle lipschitz_syntax begin
    15 notation%important lipschitz_on ("_-lipschitz'_on" [1000])
    16 end
    17 bundle no_lipschitz_syntax begin
    18 no_notation lipschitz_on ("_-lipschitz'_on" [1000])
    19 end
    20 
    21 unbundle lipschitz_syntax
    22 
    23 lemma lipschitz_onI: "L-lipschitz_on X f"
    24   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"
    25   using that by (auto simp: lipschitz_on_def)
    26 
    27 lemma lipschitz_onD:
    28   "dist (f x) (f y) \<le> L * dist x y"
    29   if "L-lipschitz_on X f" "x \<in> X" "y \<in> X"
    30   using that by (auto simp: lipschitz_on_def)
    31 
    32 lemma lipschitz_on_nonneg:
    33   "0 \<le> L" if "L-lipschitz_on X f"
    34   using that by (auto simp: lipschitz_on_def)
    35 
    36 lemma lipschitz_on_normD:
    37   "norm (f x - f y) \<le> L * norm (x - y)"
    38   if "lipschitz_on L X f" "x \<in> X" "y \<in> X"
    39   using lipschitz_onD[OF that]
    40   by (simp add: dist_norm)
    41 
    42 lemma lipschitz_on_mono: "L-lipschitz_on D f" if "M-lipschitz_on E f" "D \<subseteq> E" "M \<le> L"
    43   using that
    44   by (force simp: lipschitz_on_def intro: order_trans[OF _ mult_right_mono])
    45 
    46 lemmas lipschitz_on_subset = lipschitz_on_mono[OF _ _ order_refl]
    47   and lipschitz_on_le = lipschitz_on_mono[OF _ order_refl]
    48 
    49 lemma lipschitz_on_leI:
    50   "L-lipschitz_on X f"
    51   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"
    52     "0 \<le> L"
    53   for f::"'a::{linorder_topology, ordered_real_vector, metric_space} \<Rightarrow> 'b::metric_space"
    54 proof (rule lipschitz_onI)
    55   fix x y assume xy: "x \<in> X" "y \<in> X"
    56   consider "y \<le> x" | "x \<le> y"
    57     by (rule le_cases)
    58   then show "dist (f x) (f y) \<le> L * dist x y"
    59   proof cases
    60     case 1
    61     then have "dist (f y) (f x) \<le> L * dist y x"
    62       by (auto intro!: that xy)
    63     then show ?thesis
    64       by (simp add: dist_commute)
    65   qed (auto intro!: that xy)
    66 qed fact
    67 
    68 lemma lipschitz_on_concat:
    69   fixes a b c::real
    70   assumes f: "L-lipschitz_on {a .. b} f"
    71   assumes g: "L-lipschitz_on {b .. c} g"
    72   assumes fg: "f b = g b"
    73   shows "lipschitz_on L {a .. c} (\<lambda>x. if x \<le> b then f x else g x)"
    74     (is "lipschitz_on _ _ ?f")
    75 proof (rule lipschitz_on_leI)
    76   fix x y
    77   assume x: "x \<in> {a..c}" and y: "y \<in> {a..c}" and xy: "x \<le> y"
    78   consider "x \<le> b \<and> b < y" | "x \<ge> b \<or> y \<le> b" by arith
    79   then show "dist (?f x) (?f y) \<le> L * dist x y"
    80   proof cases
    81     case 1
    82     have "dist (f x) (g y) \<le> dist (f x) (f b) + dist (g b) (g y)"
    83       unfolding fg by (rule dist_triangle)
    84     also have "dist (f x) (f b) \<le> L * dist x b"
    85       using 1 x
    86       by (auto intro!: lipschitz_onD[OF f])
    87     also have "dist (g b) (g y) \<le> L * dist b y"
    88       using 1 x y
    89       by (auto intro!: lipschitz_onD[OF g] lipschitz_onD[OF f])
    90     finally have "dist (f x) (g y) \<le> L * dist x b + L * dist b y"
    91       by simp
    92     also have "\<dots> = L * (dist x b + dist b y)"
    93       by (simp add: algebra_simps)
    94     also have "dist x b + dist b y = dist x y"
    95       using 1 x y
    96       by (auto simp: dist_real_def abs_real_def)
    97     finally show ?thesis
    98       using 1 by simp
    99   next
   100     case 2
   101     with lipschitz_onD[OF f, of x y] lipschitz_onD[OF g, of x y] x y xy
   102     show ?thesis
   103       by (auto simp: fg)
   104   qed
   105 qed (rule lipschitz_on_nonneg[OF f])
   106 
   107 lemma lipschitz_on_concat_max:
   108   fixes a b c::real
   109   assumes f: "L-lipschitz_on {a .. b} f"
   110   assumes g: "M-lipschitz_on {b .. c} g"
   111   assumes fg: "f b = g b"
   112   shows "(max L M)-lipschitz_on {a .. c} (\<lambda>x. if x \<le> b then f x else g x)"
   113 proof -
   114   have "lipschitz_on (max L M) {a .. b} f" "lipschitz_on (max L M) {b .. c} g"
   115     by (auto intro!: lipschitz_on_mono[OF f order_refl] lipschitz_on_mono[OF g order_refl])
   116   from lipschitz_on_concat[OF this fg] show ?thesis .
   117 qed
   118 
   119 
   120 subsubsection \<open>Continuity\<close>
   121 
   122 proposition lipschitz_on_uniformly_continuous:
   123   assumes "L-lipschitz_on X f"
   124   shows "uniformly_continuous_on X f"
   125   unfolding uniformly_continuous_on_def
   126 proof safe
   127   fix e::real
   128   assume "0 < e"
   129   from assms have l: "(L+1)-lipschitz_on X f"
   130     by (rule lipschitz_on_mono) auto
   131   show "\<exists>d>0. \<forall>x\<in>X. \<forall>x'\<in>X. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
   132     using lipschitz_onD[OF l] lipschitz_on_nonneg[OF assms] \<open>0 < e\<close>
   133     by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps)
   134 qed
   135 
   136 proposition lipschitz_on_continuous_on:
   137   "continuous_on X f" if "L-lipschitz_on X f"
   138   by (rule uniformly_continuous_imp_continuous[OF lipschitz_on_uniformly_continuous[OF that]])
   139 
   140 lemma lipschitz_on_continuous_within:
   141   "continuous (at x within X) f" if "L-lipschitz_on X f" "x \<in> X"
   142   using lipschitz_on_continuous_on[OF that(1)] that(2)
   143   by (auto simp: continuous_on_eq_continuous_within)
   144 
   145 subsubsection \<open>Differentiable functions\<close>
   146 
   147 proposition bounded_derivative_imp_lipschitz:
   148   assumes "\<And>x. x \<in> X \<Longrightarrow> (f has_derivative f' x) (at x within X)"
   149   assumes convex: "convex X"
   150   assumes "\<And>x. x \<in> X \<Longrightarrow> onorm (f' x) \<le> C" "0 \<le> C"
   151   shows "C-lipschitz_on X f"
   152 proof (rule lipschitz_onI)
   153   show "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> C * dist x y"
   154     by (auto intro!: assms differentiable_bound[unfolded dist_norm[symmetric], OF convex])
   155 qed fact
   156 
   157 
   158 subsubsection%unimportant \<open>Structural introduction rules\<close>
   159 
   160 named_theorems lipschitz_intros "structural introduction rules for Lipschitz controls"
   161 
   162 lemma lipschitz_on_compose [lipschitz_intros]:
   163   "(D * C)-lipschitz_on U (g o f)"
   164   if f: "C-lipschitz_on U f" and g: "D-lipschitz_on (f`U) g"
   165 proof (rule lipschitz_onI)
   166   show "D* C \<ge> 0" using lipschitz_on_nonneg[OF f] lipschitz_on_nonneg[OF g] by auto
   167   fix x y assume H: "x \<in> U" "y \<in> U"
   168   have "dist (g (f x)) (g (f y)) \<le> D * dist (f x) (f y)"
   169     apply (rule lipschitz_onD[OF g]) using H by auto
   170   also have "... \<le> D * C * dist x y"
   171     using mult_left_mono[OF lipschitz_onD(1)[OF f H] lipschitz_on_nonneg[OF g]] by auto
   172   finally show "dist ((g \<circ> f) x) ((g \<circ> f) y) \<le> D * C* dist x y"
   173     unfolding comp_def by (auto simp add: mult.commute)
   174 qed
   175 
   176 lemma lipschitz_on_compose2:
   177   "(D * C)-lipschitz_on U (\<lambda>x. g (f x))"
   178   if "C-lipschitz_on U f" "D-lipschitz_on (f`U) g"
   179   using lipschitz_on_compose[OF that] by (simp add: o_def)
   180 
   181 lemma lipschitz_on_cong[cong]:
   182   "C-lipschitz_on U g \<longleftrightarrow> D-lipschitz_on V f"
   183   if "C = D" "U = V" "\<And>x. x \<in> V \<Longrightarrow> g x = f x"
   184   using that by (auto simp: lipschitz_on_def)
   185 
   186 lemma lipschitz_on_transform:
   187   "C-lipschitz_on U g"
   188   if "C-lipschitz_on U f"
   189     "\<And>x. x \<in> U \<Longrightarrow> g x = f x"
   190   using that
   191   by simp
   192 
   193 lemma lipschitz_on_empty_iff[simp]: "C-lipschitz_on {} f \<longleftrightarrow> C \<ge> 0"
   194   by (auto simp: lipschitz_on_def)
   195 
   196 lemma lipschitz_on_insert_iff[simp]:
   197   "C-lipschitz_on (insert y X) f \<longleftrightarrow>
   198     C-lipschitz_on X f \<and> (\<forall>x \<in> X. dist (f x) (f y) \<le> C * dist x y)"
   199   by (auto simp: lipschitz_on_def dist_commute)
   200 
   201 lemma lipschitz_on_singleton [lipschitz_intros]: "C \<ge> 0 \<Longrightarrow> C-lipschitz_on {x} f"
   202   and lipschitz_on_empty [lipschitz_intros]: "C \<ge> 0 \<Longrightarrow> C-lipschitz_on {} f"
   203   by simp_all
   204 
   205 lemma lipschitz_on_id [lipschitz_intros]: "1-lipschitz_on U (\<lambda>x. x)"
   206   by (auto simp: lipschitz_on_def)
   207 
   208 lemma lipschitz_on_constant [lipschitz_intros]: "0-lipschitz_on U (\<lambda>x. c)"
   209   by (auto simp: lipschitz_on_def)
   210 
   211 lemma lipschitz_on_add [lipschitz_intros]:
   212   fixes f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
   213   assumes "C-lipschitz_on U f"
   214     "D-lipschitz_on U g"
   215   shows "(C+D)-lipschitz_on U (\<lambda>x. f x + g x)"
   216 proof (rule lipschitz_onI)
   217   show "C + D \<ge> 0"
   218     using lipschitz_on_nonneg[OF assms(1)] lipschitz_on_nonneg[OF assms(2)] by auto
   219   fix x y assume H: "x \<in> U" "y \<in> U"
   220   have "dist (f x + g x) (f y + g y) \<le> dist (f x) (f y) + dist (g x) (g y)"
   221     by (simp add: dist_triangle_add)
   222   also have "... \<le> C * dist x y + D * dist x y"
   223     using lipschitz_onD(1)[OF assms(1) H] lipschitz_onD(1)[OF assms(2) H] by auto
   224   finally show "dist (f x + g x) (f y + g y) \<le> (C+D) * dist x y" by (auto simp add: algebra_simps)
   225 qed
   226 
   227 lemma lipschitz_on_cmult [lipschitz_intros]:
   228   fixes f::"'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   229   assumes "C-lipschitz_on U f"
   230   shows "(abs(a) * C)-lipschitz_on U (\<lambda>x. a *\<^sub>R f x)"
   231 proof (rule lipschitz_onI)
   232   show "abs(a) * C \<ge> 0" using lipschitz_on_nonneg[OF assms(1)] by auto
   233   fix x y assume H: "x \<in> U" "y \<in> U"
   234   have "dist (a *\<^sub>R f x) (a *\<^sub>R f y) = abs(a) * dist (f x) (f y)"
   235     by (metis dist_norm norm_scaleR real_vector.scale_right_diff_distrib)
   236   also have "... \<le> abs(a) * C * dist x y"
   237     using lipschitz_onD(1)[OF assms(1) H] by (simp add: Groups.mult_ac(1) mult_left_mono)
   238   finally show "dist (a *\<^sub>R f x) (a *\<^sub>R f y) \<le> \<bar>a\<bar> * C * dist x y" by auto
   239 qed
   240 
   241 lemma lipschitz_on_cmult_real [lipschitz_intros]:
   242   fixes f::"'a::metric_space \<Rightarrow> real"
   243   assumes "C-lipschitz_on U f"
   244   shows "(abs(a) * C)-lipschitz_on U (\<lambda>x. a * f x)"
   245   using lipschitz_on_cmult[OF assms] by auto
   246 
   247 lemma lipschitz_on_cmult_nonneg [lipschitz_intros]:
   248   fixes f::"'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   249   assumes "C-lipschitz_on U f"
   250     "a \<ge> 0"
   251   shows "(a * C)-lipschitz_on U (\<lambda>x. a *\<^sub>R f x)"
   252   using lipschitz_on_cmult[OF assms(1), of a] assms(2) by auto
   253 
   254 lemma lipschitz_on_cmult_real_nonneg [lipschitz_intros]:
   255   fixes f::"'a::metric_space \<Rightarrow> real"
   256   assumes "C-lipschitz_on U f"
   257     "a \<ge> 0"
   258   shows "(a * C)-lipschitz_on U (\<lambda>x. a * f x)"
   259   using lipschitz_on_cmult_nonneg[OF assms] by auto
   260 
   261 lemma lipschitz_on_cmult_upper [lipschitz_intros]:
   262   fixes f::"'a::metric_space \<Rightarrow> 'b::real_normed_vector"
   263   assumes "C-lipschitz_on U f"
   264     "abs(a) \<le> D"
   265   shows "(D * C)-lipschitz_on U (\<lambda>x. a *\<^sub>R f x)"
   266   apply (rule lipschitz_on_mono[OF lipschitz_on_cmult[OF assms(1), of a], of _ "D * C"])
   267   using assms(2) lipschitz_on_nonneg[OF assms(1)] mult_right_mono by auto
   268 
   269 lemma lipschitz_on_cmult_real_upper [lipschitz_intros]:
   270   fixes f::"'a::metric_space \<Rightarrow> real"
   271   assumes "C-lipschitz_on U f"
   272     "abs(a) \<le> D"
   273   shows "(D * C)-lipschitz_on U (\<lambda>x. a * f x)"
   274   using lipschitz_on_cmult_upper[OF assms] by auto
   275 
   276 lemma lipschitz_on_minus[lipschitz_intros]:
   277   fixes f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
   278   assumes "C-lipschitz_on U f"
   279   shows "C-lipschitz_on U (\<lambda>x. - f x)"
   280   by (metis (mono_tags, lifting) assms dist_minus lipschitz_on_def)
   281 
   282 lemma lipschitz_on_minus_iff[simp]:
   283   "L-lipschitz_on X (\<lambda>x. - f x) \<longleftrightarrow> L-lipschitz_on X f"
   284   "L-lipschitz_on X (- f) \<longleftrightarrow> L-lipschitz_on X f"
   285   for f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
   286   using lipschitz_on_minus[of L X f] lipschitz_on_minus[of L X "-f"]
   287   by auto
   288 
   289 lemma lipschitz_on_diff[lipschitz_intros]:
   290   fixes f::"'a::metric_space \<Rightarrow>'b::real_normed_vector"
   291   assumes "C-lipschitz_on U f" "D-lipschitz_on U g"
   292   shows "(C + D)-lipschitz_on U (\<lambda>x. f x - g x)"
   293   using lipschitz_on_add[OF assms(1) lipschitz_on_minus[OF assms(2)]] by auto
   294 
   295 lemma lipschitz_on_closure [lipschitz_intros]:
   296   assumes "C-lipschitz_on U f" "continuous_on (closure U) f"
   297   shows "C-lipschitz_on (closure U) f"
   298 proof (rule lipschitz_onI)
   299   show "C \<ge> 0" using lipschitz_on_nonneg[OF assms(1)] by simp
   300   fix x y assume "x \<in> closure U" "y \<in> closure U"
   301   obtain u v::"nat \<Rightarrow> 'a" where *: "\<And>n. u n \<in> U" "u \<longlonglongrightarrow> x"
   302                                    "\<And>n. v n \<in> U" "v \<longlonglongrightarrow> y"
   303     using \<open>x \<in> closure U\<close> \<open>y \<in> closure U\<close> unfolding closure_sequential by blast
   304   have a: "(\<lambda>n. f (u n)) \<longlonglongrightarrow> f x"
   305     using *(1) *(2) \<open>x \<in> closure U\<close> \<open>continuous_on (closure U) f\<close>
   306     unfolding comp_def continuous_on_closure_sequentially[of U f] by auto
   307   have b: "(\<lambda>n. f (v n)) \<longlonglongrightarrow> f y"
   308     using *(3) *(4) \<open>y \<in> closure U\<close> \<open>continuous_on (closure U) f\<close>
   309     unfolding comp_def continuous_on_closure_sequentially[of U f] by auto
   310   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)"
   311     by (intro tendsto_intros * a b)
   312   have "C * dist (u n) (v n) - dist (f (u n)) (f (v n)) \<ge> 0" for n
   313     using lipschitz_onD(1)[OF assms(1) \<open>u n \<in> U\<close> \<open>v n \<in> U\<close>] by simp
   314   then have "C * dist x y - dist (f x) (f y) \<ge> 0" using LIMSEQ_le_const[OF l, of 0] by auto
   315   then show "dist (f x) (f y) \<le> C * dist x y" by auto
   316 qed
   317 
   318 lemma lipschitz_on_Pair[lipschitz_intros]:
   319   assumes f: "L-lipschitz_on A f"
   320   assumes g: "M-lipschitz_on A g"
   321   shows "(sqrt (L\<^sup>2 + M\<^sup>2))-lipschitz_on A (\<lambda>a. (f a, g a))"
   322 proof (rule lipschitz_onI, goal_cases)
   323   case (1 x y)
   324   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)"
   325     by (auto simp add: dist_Pair_Pair real_le_lsqrt)
   326   also have "\<dots> \<le> sqrt ((L * dist x y)\<^sup>2 + (M * dist x y)\<^sup>2)"
   327     by (auto intro!: real_sqrt_le_mono add_mono power_mono 1 lipschitz_onD f g)
   328   also have "\<dots> \<le> sqrt (L\<^sup>2 + M\<^sup>2) * dist x y"
   329     by (auto simp: power_mult_distrib ring_distribs[symmetric] real_sqrt_mult)
   330   finally show ?case .
   331 qed simp
   332 
   333 lemma lipschitz_extend_closure:
   334   fixes f::"('a::metric_space) \<Rightarrow> ('b::complete_space)"
   335   assumes "C-lipschitz_on U f"
   336   shows "\<exists>g. C-lipschitz_on (closure U) g \<and> (\<forall>x\<in>U. g x = f x)"
   337 proof -
   338   obtain g where g: "\<And>x. x \<in> U \<Longrightarrow> g x = f x" "uniformly_continuous_on (closure U) g"
   339     using uniformly_continuous_on_extension_on_closure[OF lipschitz_on_uniformly_continuous[OF assms]] by metis
   340   have "C-lipschitz_on (closure U) g"
   341     apply (rule lipschitz_on_closure, rule lipschitz_on_transform[OF assms])
   342     using g uniformly_continuous_imp_continuous[OF g(2)] by auto
   343   then show ?thesis using g(1) by auto
   344 qed
   345 
   346 lemma (in bounded_linear) lipschitz_boundE:
   347   obtains B where "B-lipschitz_on A f"
   348 proof -
   349   from nonneg_bounded
   350   obtain B where B: "B \<ge> 0" "\<And>x. norm (f x) \<le> B * norm x"
   351     by (auto simp: ac_simps)
   352   have "B-lipschitz_on A f"
   353     by (auto intro!: lipschitz_onI B simp: dist_norm diff[symmetric])
   354   thus ?thesis ..
   355 qed
   356 
   357 
   358 subsection \<open>Local Lipschitz continuity\<close>
   359 
   360 text \<open>Given a function defined on a real interval, it is Lipschitz-continuous if and only if
   361 it is locally so, as proved in the following lemmas. It is useful especially for
   362 piecewise-defined functions: if each piece is Lipschitz, then so is the whole function.
   363 The same goes for functions defined on geodesic spaces, or more generally on geodesic subsets
   364 in a metric space (for instance convex subsets in a real vector space), and this follows readily
   365 from the real case, but we will not prove it explicitly.
   366 
   367 We give several variations around this statement. This is essentially a connectedness argument.\<close>
   368 
   369 lemma locally_lipschitz_imp_lispchitz_aux:
   370   fixes f::"real \<Rightarrow> ('a::metric_space)"
   371   assumes "a \<le> b"
   372           "continuous_on {a..b} f"
   373           "\<And>x. x \<in> {a..<b} \<Longrightarrow> \<exists>y \<in> {x<..b}. dist (f y) (f x) \<le> M * (y-x)"
   374   shows "dist (f b) (f a) \<le> M * (b-a)"
   375 proof -
   376   define A where "A = {x \<in> {a..b}. dist (f x) (f a) \<le> M * (x-a)}"
   377   have *: "A = (\<lambda>x. M * (x-a) - dist (f x) (f a))-`{0..} \<inter> {a..b}"
   378     unfolding A_def by auto
   379   have "a \<in> A" unfolding A_def using \<open>a \<le> b\<close> by auto
   380   then have "A \<noteq> {}" by auto
   381   moreover have "bdd_above A" unfolding A_def by auto
   382   moreover have "closed A" unfolding * by (rule closed_vimage_Int, auto intro!: continuous_intros assms)
   383   ultimately have "Sup A \<in> A" by (rule closed_contains_Sup)
   384   have "Sup A = b"
   385   proof (rule ccontr)
   386     assume "Sup A \<noteq> b"
   387     define x where "x = Sup A"
   388     have I: "dist (f x) (f a) \<le> M * (x-a)" using \<open>Sup A \<in> A\<close> x_def A_def by auto
   389     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
   390     then obtain y where J: "y \<in> {x<..b}" "dist (f y) (f x) \<le> M * (y-x)" using assms(3) by blast
   391     have "dist (f y) (f a) \<le> dist (f y) (f x) + dist (f x) (f a)" by (rule dist_triangle)
   392     also have "... \<le> M * (y-x) + M * (x-a)" using I J(2) by auto
   393     finally have "dist (f y) (f a) \<le> M * (y-a)" by (auto simp add: algebra_simps)
   394     then have "y \<in> A" unfolding A_def using \<open>y \<in> {x<..b}\<close> \<open>x \<in> {a..<b}\<close> by auto
   395     then have "y \<le> Sup A" by (rule cSup_upper, auto simp: A_def)
   396     then show False using \<open>y \<in> {x<..b}\<close> x_def by auto
   397   qed
   398   then show ?thesis using \<open>Sup A \<in> A\<close> A_def by auto
   399 qed
   400 
   401 lemma locally_lipschitz_imp_lipschitz:
   402   fixes f::"real \<Rightarrow> ('a::metric_space)"
   403   assumes "continuous_on {a..b} f"
   404           "\<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)"
   405           "M \<ge> 0"
   406   shows "lipschitz_on M {a..b} f"
   407 proof (rule lipschitz_onI[OF _ \<open>M \<ge> 0\<close>])
   408   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
   409   proof (rule locally_lipschitz_imp_lispchitz_aux, simp add: \<open>s \<le> t\<close>)
   410     show "continuous_on {s..t} f" using continuous_on_subset[OF assms(1)] that by auto
   411     fix x assume "x \<in> {s..<t}"
   412     then have "x \<in> {a..<b}" using that by auto
   413     show "\<exists>z\<in>{x<..t}. dist (f z) (f x) \<le> M * (z - x)"
   414       using assms(2)[OF \<open>x \<in> {a..<b}\<close>, of t] \<open>x \<in> {s..<t}\<close> by auto
   415   qed
   416   fix x y assume "x \<in> {a..b}" "y \<in> {a..b}"
   417   consider "x \<le> y" | "y \<le> x" by linarith
   418   then show "dist (f x) (f y) \<le> M * dist x y"
   419     apply (cases)
   420     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>]
   421     by (auto simp add: dist_commute dist_real_def)
   422 qed
   423 
   424 text \<open>We deduce that if a function is Lipschitz on finitely many closed sets on the real line, then
   425 it is Lipschitz on any interval contained in their union. The difficulty in the proof is to show
   426 that any point \<open>z\<close> in this interval (except the maximum) has a point arbitrarily close to it on its
   427 right which is contained in a common initial closed set. Otherwise, we show that there is a small
   428 interval \<open>(z, T)\<close> which does not intersect any of the initial closed sets, a contradiction.\<close>
   429 
   430 proposition lipschitz_on_closed_Union:
   431   assumes "\<And>i. i \<in> I \<Longrightarrow> lipschitz_on M (U i) f"
   432           "\<And>i. i \<in> I \<Longrightarrow> closed (U i)"
   433           "finite I"
   434           "M \<ge> 0"
   435           "{u..(v::real)} \<subseteq> (\<Union>i\<in>I. U i)"
   436   shows "lipschitz_on M {u..v} f"
   437 proof (rule locally_lipschitz_imp_lipschitz[OF _ _ \<open>M \<ge> 0\<close>])
   438   have *: "continuous_on (U i) f" if "i \<in> I" for i
   439     by (rule lipschitz_on_continuous_on[OF assms(1)[OF \<open>i\<in> I\<close>]])
   440   have "continuous_on (\<Union>i\<in>I. U i) f"
   441     apply (rule continuous_on_closed_Union) using \<open>finite I\<close> * assms(2) by auto
   442   then show "continuous_on {u..v} f"
   443     using \<open>{u..(v::real)} \<subseteq> (\<Union>i\<in>I. U i)\<close> continuous_on_subset by auto
   444 
   445   fix z Z assume z: "z \<in> {u..<v}" "z < Z"
   446   then have "u \<le> v" by auto
   447   define T where "T = min Z v"
   448   then have T: "T > z" "T \<le> v" "T \<ge> u" "T \<le> Z" using z by auto
   449   define A where "A = (\<Union>i\<in> I \<inter> {i. U i \<inter> {z<..T} \<noteq> {}}. U i \<inter> {z..T})"
   450   have a: "closed A"
   451     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
   452   have b: "bdd_below A" unfolding A_def using \<open>finite I\<close> by auto
   453   have "\<exists>i \<in> I. T \<in> U i" using \<open>{u..v} \<subseteq> (\<Union>i\<in>I. U i)\<close> T by auto
   454   then have c: "T \<in> A" unfolding A_def using T by (auto, fastforce)
   455   have "Inf A \<ge> z"
   456     apply (rule cInf_greatest, auto) using c unfolding A_def by auto
   457   moreover have "Inf A \<le> z"
   458   proof (rule ccontr)
   459     assume "\<not>(Inf A \<le> z)"
   460     then obtain w where w: "w > z" "w < Inf A" by (meson dense not_le_imp_less)
   461     have "Inf A \<le> T" using a b c by (simp add: cInf_lower)
   462     then have "w \<le> T" using w by auto
   463     then have "w \<in> {u..v}" using w \<open>z \<in> {u..<v}\<close> T by auto
   464     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
   465     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
   466     then have "w \<in> A" unfolding A_def using \<open>j \<in> I\<close> by auto
   467     then have "Inf A \<le> w" using a b by (simp add: cInf_lower)
   468     then show False using w by auto
   469   qed
   470   ultimately have "Inf A = z" by simp
   471   moreover have "Inf A \<in> A"
   472     apply (rule closed_contains_Inf) using a b c by auto
   473   ultimately have "z \<in> A" by simp
   474   then obtain i where i: "i \<in> I" "U i \<inter> {z<..T} \<noteq> {}" "z \<in> U i" unfolding A_def by auto
   475   then obtain t where "t \<in> U i \<inter> {z<..T}" by blast
   476   then have "dist (f t) (f z) \<le> M * (t - z)"
   477     using lipschitz_onD(1)[OF assms(1)[of i], of t z] i dist_real_def by auto
   478   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
   479 qed
   480 
   481 
   482 subsection \<open>Local Lipschitz continuity (uniform for a family of functions)\<close>
   483 
   484 definition%important local_lipschitz::
   485   "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c::metric_space) \<Rightarrow> bool"
   486   where
   487   "local_lipschitz T X f \<equiv> \<forall>x \<in> X. \<forall>t \<in> T.
   488     \<exists>u>0. \<exists>L. \<forall>t \<in> cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
   489 
   490 lemma local_lipschitzI:
   491   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)"
   492   shows "local_lipschitz T X f"
   493   using assms
   494   unfolding local_lipschitz_def
   495   by auto
   496 
   497 lemma local_lipschitzE:
   498   assumes local_lipschitz: "local_lipschitz T X f"
   499   assumes "t \<in> T" "x \<in> X"
   500   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)"
   501   using assms local_lipschitz_def
   502   by metis
   503 
   504 lemma local_lipschitz_continuous_on:
   505   assumes local_lipschitz: "local_lipschitz T X f"
   506   assumes "t \<in> T"
   507   shows "continuous_on X (f t)"
   508   unfolding continuous_on_def
   509 proof safe
   510   fix x assume "x \<in> X"
   511   from local_lipschitzE[OF local_lipschitz \<open>t \<in> T\<close> \<open>x \<in> X\<close>] obtain u L
   512     where "0 < u"
   513     and L: "\<And>s. s \<in> cball t u \<inter> T \<Longrightarrow> L-lipschitz_on (cball x u \<inter> X) (f s)"
   514     by metis
   515   have "x \<in> ball x u" using \<open>0 < u\<close> by simp
   516   from lipschitz_on_continuous_on[OF L]
   517   have tendsto: "(f t \<longlongrightarrow> f t x) (at x within cball x u \<inter> X)"
   518     using \<open>0 < u\<close> \<open>x \<in> X\<close> \<open>t \<in> T\<close>
   519     by (auto simp: continuous_on_def)
   520   moreover have "\<forall>\<^sub>F xa in at x. (xa \<in> cball x u \<inter> X) = (xa \<in> X)"
   521     using eventually_at_ball[OF \<open>0 < u\<close>, of x UNIV]
   522     by eventually_elim auto
   523   ultimately show "(f t \<longlongrightarrow> f t x) (at x within X)"
   524     by (rule Lim_transform_within_set)
   525 qed
   526 
   527 lemma
   528   local_lipschitz_compose1:
   529   assumes ll: "local_lipschitz (g ` T) X (\<lambda>t. f t)"
   530   assumes g: "continuous_on T g"
   531   shows "local_lipschitz T X (\<lambda>t. f (g t))"
   532 proof (rule local_lipschitzI)
   533   fix t x
   534   assume "t \<in> T" "x \<in> X"
   535   then have "g t \<in> g ` T" by simp
   536   from local_lipschitzE[OF assms(1) this \<open>x \<in> X\<close>]
   537   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))"
   538     by auto
   539   from g[unfolded continuous_on_eq_continuous_within, rule_format, OF \<open>t \<in> T\<close>,
   540     unfolded continuous_within_eps_delta, rule_format, OF \<open>0 < u\<close>]
   541   obtain d where d: "d>0" "\<And>x'. x'\<in>T \<Longrightarrow> dist x' t < d \<Longrightarrow> dist (g x') (g t) < u"
   542     by (auto)
   543   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))"
   544     using d \<open>0 < u\<close>
   545     by (fastforce intro: exI[where x="(min d u)/2"] exI[where x=L]
   546       intro!: less_imp_le[OF d(2)] lipschitz_on_subset[OF l] simp: dist_commute mem_ball mem_cball)
   547 qed
   548 
   549 context
   550   fixes T::"'a::metric_space set" and X f
   551   assumes local_lipschitz: "local_lipschitz T X f"
   552 begin
   553 
   554 lemma continuous_on_TimesI:
   555   assumes y: "\<And>x. x \<in> X \<Longrightarrow> continuous_on T (\<lambda>t. f t x)"
   556   shows "continuous_on (T \<times> X) (\<lambda>(t, x). f t x)"
   557   unfolding continuous_on_iff
   558 proof (safe, simp)
   559   fix a b and e::real
   560   assume H: "a \<in> T" "b \<in> X" "0 < e"
   561   hence "0 < e/2" by simp
   562   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>]
   563   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"
   564     by auto
   565 
   566   from \<open>a : T\<close> \<open>b \<in> X\<close>
   567   obtain u L where u: "0 < u"
   568     and L: "\<And>t. t \<in> cball a u \<inter> T \<Longrightarrow> L-lipschitz_on  (cball b u \<inter> X) (f t)"
   569     by (erule local_lipschitzE[OF local_lipschitz])
   570 
   571   have "a \<in> cball a u \<inter> T" by (auto simp: \<open>0 < u\<close> \<open>a \<in> T\<close> less_imp_le)
   572   from lipschitz_on_nonneg[OF L[OF \<open>a \<in> cball _ _ \<inter> _\<close>]] have "0 \<le> L" .
   573 
   574   let ?d = "Min {d, u, (e/2/(L + 1))}"
   575   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"
   576   proof (rule exI[where x = ?d], safe)
   577     show "0 < ?d"
   578       using \<open>0 \<le> L\<close> \<open>0 < u\<close> \<open>0 < e\<close> \<open>0 < d\<close>
   579       by (auto intro!: divide_pos_pos )
   580     fix x y
   581     assume "x \<in> T" "y \<in> X"
   582     assume dist_less: "dist (x, y) (a, b) < ?d"
   583     have "dist y b \<le> dist (x, y) (a, b)"
   584       using dist_snd_le[of "(x, y)" "(a, b)"]
   585       by auto
   586     also
   587     note dist_less
   588     also
   589     {
   590       note calculation
   591       also have "?d \<le> u" by simp
   592       finally have "dist y b < u" .
   593     }
   594     have "?d \<le> e/2/(L + 1)" by simp
   595     also have "(L + 1) * \<dots> \<le> e / 2"
   596       using \<open>0 < e\<close> \<open>L \<ge> 0\<close>
   597       by (auto simp: divide_simps)
   598     finally have le1: "(L + 1) * dist y b < e / 2" using \<open>L \<ge> 0\<close> by simp
   599 
   600     have "dist x a \<le> dist (x, y) (a, b)"
   601       using dist_fst_le[of "(x, y)" "(a, b)"]
   602       by auto
   603     also note dist_less
   604     finally have "dist x a < ?d" .
   605     also have "?d \<le> d" by simp
   606     finally have "dist x a < d" .
   607     note \<open>dist x a < ?d\<close>
   608     also have "?d \<le> u" by simp
   609     finally have "dist x a < u" .
   610     then have "x \<in> cball a u \<inter> T"
   611       using \<open>x \<in> T\<close>
   612       by (auto simp: dist_commute mem_cball)
   613     have "dist (f x y) (f a b) \<le> dist (f x y) (f x b) + dist (f x b) (f a b)"
   614       by (rule dist_triangle)
   615     also have "(L + 1)-lipschitz_on (cball b u \<inter> X) (f x)"
   616       using L[OF \<open>x \<in> cball a u \<inter> T\<close>]
   617       by (rule lipschitz_on_le) simp
   618     then have "dist (f x y) (f x b) \<le> (L + 1) * dist y b"
   619       apply (rule lipschitz_onD)
   620       subgoal
   621         using \<open>y \<in> X\<close> \<open>dist y b < u\<close>
   622         by (simp add: dist_commute)
   623       subgoal
   624         using \<open>0 < u\<close> \<open>b \<in> X\<close>
   625         by (simp add: )
   626       done
   627     also have "(L + 1) * dist y b \<le> e / 2"
   628       using le1 \<open>0 \<le> L\<close> by simp
   629     also have "dist (f x b) (f a b) < e / 2"
   630       by (rule d; fact)
   631     also have "e / 2 + e / 2 = e" by simp
   632     finally show "dist (f x y) (f a b) < e" by simp
   633   qed
   634 qed
   635 
   636 lemma local_lipschitz_compact_implies_lipschitz:
   637   assumes "compact X" "compact T"
   638   assumes cont: "\<And>x. x \<in> X \<Longrightarrow> continuous_on T (\<lambda>t. f t x)"
   639   obtains L where "\<And>t. t \<in> T \<Longrightarrow> L-lipschitz_on X (f t)"
   640 proof -
   641   {
   642     assume *: "\<And>n::nat. \<not>(\<forall>t\<in>T. n-lipschitz_on X (f t))"
   643     {
   644       fix n::nat
   645       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"
   646         by (force simp: lipschitz_on_def)
   647     } then obtain t and x y::"nat \<Rightarrow> 'b" where xy: "\<And>n. x n \<in> X" "\<And>n. y n \<in> X"
   648       and t: "\<And>n. t n \<in> T"
   649       and d: "\<And>n. dist (f (t n) (y n)) (f (t n) (x n)) > n * dist (y n) (x n)"
   650       by metis
   651     from xy assms obtain lx rx where lx': "lx \<in> X" "strict_mono (rx :: nat \<Rightarrow> nat)" "(x o rx) \<longlonglongrightarrow> lx"
   652       by (metis compact_def)
   653     with xy have "\<And>n. (y o rx) n \<in> X" by auto
   654     with assms obtain ly ry where ly': "ly \<in> X" "strict_mono (ry :: nat \<Rightarrow> nat)" "((y o rx) o ry) \<longlonglongrightarrow> ly"
   655       by (metis compact_def)
   656     with t have "\<And>n. ((t o rx) o ry) n \<in> T" by simp
   657     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"
   658       by (metis compact_def)
   659     from lx' ly'
   660     have lx: "(x o (rx o ry o rt)) \<longlonglongrightarrow> lx" (is "?x \<longlonglongrightarrow> _")
   661       and ly: "(y o (rx o ry o rt)) \<longlonglongrightarrow> ly" (is "?y \<longlonglongrightarrow> _")
   662       and lt: "(t o (rx o ry o rt)) \<longlonglongrightarrow> lt" (is "?t \<longlonglongrightarrow> _")
   663       subgoal by (simp add: LIMSEQ_subseq_LIMSEQ o_assoc lt'(2))
   664       subgoal by (simp add: LIMSEQ_subseq_LIMSEQ ly'(3) o_assoc lt'(2))
   665       subgoal by (simp add: o_assoc lt'(3))
   666       done
   667     hence "(\<lambda>n. dist (?y n) (?x n)) \<longlonglongrightarrow> dist ly lx"
   668       by (metis tendsto_dist)
   669     moreover
   670     let ?S = "(\<lambda>(t, x). f t x) ` (T \<times> X)"
   671     have "eventually (\<lambda>n::nat. n > 0) sequentially"
   672       by (metis eventually_at_top_dense)
   673     hence "eventually (\<lambda>n. norm (dist (?y n) (?x n)) \<le> norm (\<bar>diameter ?S\<bar> / n) * 1) sequentially"
   674     proof eventually_elim
   675       case (elim n)
   676       have "0 < rx (ry (rt n))" using \<open>0 < n\<close>
   677         by (metis dual_order.strict_trans1 lt'(2) lx'(2) ly'(2) seq_suble)
   678       have compact: "compact ?S"
   679         by (auto intro!: compact_continuous_image continuous_on_subset[OF continuous_on_TimesI]
   680           compact_Times \<open>compact X\<close> \<open>compact T\<close> cont)
   681       have "norm (dist (?y n) (?x n)) = dist (?y n) (?x n)" by simp
   682       also
   683       from this elim d[of "rx (ry (rt n))"]
   684       have "\<dots> < dist (f (?t n) (?y n)) (f (?t n) (?x n)) / rx (ry (rt (n)))"
   685         using lx'(2) ly'(2) lt'(2) \<open>0 < rx _\<close>
   686         by (auto simp add: divide_simps algebra_simps strict_mono_def)
   687       also have "\<dots> \<le> diameter ?S / n"
   688         by (force intro!: \<open>0 < n\<close> strict_mono_def xy diameter_bounded_bound frac_le
   689           compact_imp_bounded compact t
   690           intro: le_trans[OF seq_suble[OF lt'(2)]]
   691             le_trans[OF seq_suble[OF ly'(2)]]
   692             le_trans[OF seq_suble[OF lx'(2)]])
   693       also have "\<dots> \<le> abs (diameter ?S) / n"
   694         by (auto intro!: divide_right_mono)
   695       finally show ?case by simp
   696     qed
   697     with _ have "(\<lambda>n. dist (?y n) (?x n)) \<longlonglongrightarrow> 0"
   698       by (rule tendsto_0_le)
   699         (metis tendsto_divide_0[OF tendsto_const] filterlim_at_top_imp_at_infinity
   700           filterlim_real_sequentially)
   701     ultimately have "lx = ly"
   702       using LIMSEQ_unique by fastforce
   703     with assms lx' have "lx \<in> X" by auto
   704     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)"
   705       by (erule local_lipschitzE[OF local_lipschitz])
   706     hence "L \<ge> 0" by (force intro!: lipschitz_on_nonneg \<open>lt \<in> T\<close>)
   707 
   708     from L lt ly lx \<open>lx = ly\<close>
   709     have
   710       "eventually (\<lambda>n. ?t n \<in> ball lt u) sequentially"
   711       "eventually (\<lambda>n. ?y n \<in> ball lx u) sequentially"
   712       "eventually (\<lambda>n. ?x n \<in> ball lx u) sequentially"
   713       by (auto simp: dist_commute Lim mem_ball)
   714     moreover have "eventually (\<lambda>n. n > L) sequentially"
   715       by (metis filterlim_at_top_dense filterlim_real_sequentially)
   716     ultimately
   717     have "eventually (\<lambda>_. False) sequentially"
   718     proof eventually_elim
   719       case (elim n)
   720       hence "dist (f (?t n) (?y n)) (f (?t n) (?x n)) \<le> L * dist (?y n) (?x n)"
   721         using assms xy t
   722         unfolding dist_norm[symmetric]
   723         by (intro lipschitz_onD[OF L(2)]) (auto simp: mem_ball mem_cball)
   724       also have "\<dots> \<le> n * dist (?y n) (?x n)"
   725         using elim by (intro mult_right_mono) auto
   726       also have "\<dots> \<le> rx (ry (rt n)) * dist (?y n) (?x n)"
   727         by (intro mult_right_mono[OF _ zero_le_dist])
   728            (meson lt'(2) lx'(2) ly'(2) of_nat_le_iff order_trans seq_suble)
   729       also have "\<dots> < dist (f (?t n) (?y n)) (f (?t n) (?x n))"
   730         by (auto intro!: d)
   731       finally show ?case by simp
   732     qed
   733     hence False
   734       by simp
   735   } then obtain L where "\<And>t. t \<in> T \<Longrightarrow> L-lipschitz_on X (f t)"
   736     by metis
   737   thus ?thesis ..
   738 qed
   739 
   740 lemma local_lipschitz_subset:
   741   assumes "S \<subseteq> T" "Y \<subseteq> X"
   742   shows "local_lipschitz S Y f"
   743 proof (rule local_lipschitzI)
   744   fix t x assume "t \<in> S" "x \<in> Y"
   745   then have "t \<in> T" "x \<in> X" using assms by auto
   746   from local_lipschitzE[OF local_lipschitz, OF this]
   747   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)"
   748     by blast
   749   show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> S. L-lipschitz_on (cball x u \<inter> Y) (f t)"
   750     using assms
   751     by (auto intro: exI[where x=u] exI[where x=L]
   752         intro!: u lipschitz_on_subset[OF _ Int_mono[OF order_refl \<open>Y \<subseteq> X\<close>]] L)
   753 qed
   754 
   755 end
   756 
   757 lemma local_lipschitz_minus:
   758   fixes f::"'a::metric_space \<Rightarrow> 'b::metric_space \<Rightarrow> 'c::real_normed_vector"
   759   shows "local_lipschitz T X (\<lambda>t x. - f t x) = local_lipschitz T X f"
   760   by (auto simp: local_lipschitz_def lipschitz_on_minus)
   761 
   762 lemma local_lipschitz_PairI:
   763   assumes f: "local_lipschitz A B (\<lambda>a b. f a b)"
   764   assumes g: "local_lipschitz A B (\<lambda>a b. g a b)"
   765   shows "local_lipschitz A B (\<lambda>a b. (f a b, g a b))"
   766 proof (rule local_lipschitzI)
   767   fix t x assume "t \<in> A" "x \<in> B"
   768   from local_lipschitzE[OF f this] local_lipschitzE[OF g this]
   769   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))"
   770     "0 < v" "(\<And>s. s \<in> cball t v \<inter> A \<Longrightarrow> M-lipschitz_on (cball x v \<inter> B) (g s))"
   771     by metis
   772   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))"
   773     by (intro exI[where x="min u v"])
   774       (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair simp: mem_cball)
   775 qed
   776 
   777 lemma local_lipschitz_constI: "local_lipschitz S T (\<lambda>t x. f t)"
   778   by (auto simp: intro!: local_lipschitzI lipschitz_on_constant intro: exI[where x=1])
   779 
   780 lemma (in bounded_linear) local_lipschitzI:
   781   shows "local_lipschitz A B (\<lambda>_. f)"
   782 proof (rule local_lipschitzI, goal_cases)
   783   case (1 t x)
   784   from lipschitz_boundE[of "(cball x 1 \<inter> B)"] obtain C where "C-lipschitz_on (cball x 1 \<inter> B) f" by auto
   785   then show ?case
   786     by (auto intro: exI[where x=1])
   787 qed
   788 
   789 proposition c1_implies_local_lipschitz:
   790   fixes T::"real set" and X::"'a::{banach,heine_borel} set"
   791     and f::"real \<Rightarrow> 'a \<Rightarrow> 'a"
   792   assumes f': "\<And>t x. t \<in> T \<Longrightarrow> x \<in> X \<Longrightarrow> (f t has_derivative blinfun_apply (f' (t, x))) (at x)"
   793   assumes cont_f': "continuous_on (T \<times> X) f'"
   794   assumes "open T"
   795   assumes "open X"
   796   shows "local_lipschitz T X f"
   797 proof (rule local_lipschitzI)
   798   fix t x
   799   assume "t \<in> T" "x \<in> X"
   800   from open_contains_cball[THEN iffD1, OF \<open>open X\<close>, rule_format, OF \<open>x \<in> X\<close>]
   801   obtain u where u: "u > 0" "cball x u \<subseteq> X" by auto
   802   moreover
   803   from open_contains_cball[THEN iffD1, OF \<open>open T\<close>, rule_format, OF \<open>t \<in> T\<close>]
   804   obtain v where v: "v > 0" "cball t v \<subseteq> T" by auto
   805   ultimately
   806   have "compact (cball t v \<times> cball x u)" "cball t v \<times> cball x u \<subseteq> T \<times> X"
   807     by (auto intro!: compact_Times)
   808   then have "compact (f' ` (cball t v \<times> cball x u))"
   809     by (auto intro!: compact_continuous_image continuous_on_subset[OF cont_f'])
   810   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"
   811     by (auto dest!: compact_imp_bounded simp: bounded_pos simp: mem_ball)
   812 
   813   have lipschitz: "B-lipschitz_on (cball x (min u v) \<inter> X) (f s)" if s: "s \<in> cball t v" for s
   814   proof -
   815     note s
   816     also note \<open>cball t v \<subseteq> T\<close>
   817     finally
   818     have deriv: "\<And>y. y \<in> cball x u \<Longrightarrow> (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
   819       using \<open>_ \<subseteq> X\<close>
   820       by (auto intro!: has_derivative_at_withinI[OF f'])
   821     have "norm (f s y - f s z) \<le> B * norm (y - z)"
   822       if "y \<in> cball x u" "z \<in> cball x u"
   823       for y z
   824       using s that
   825       by (intro differentiable_bound[OF convex_cball deriv])
   826         (auto intro!: B  simp: norm_blinfun.rep_eq[symmetric] mem_cball)
   827     then show ?thesis
   828       using \<open>0 < B\<close>
   829       by (auto intro!: lipschitz_onI simp: dist_norm mem_cball)
   830   qed
   831   show "\<exists>u>0. \<exists>L. \<forall>t\<in>cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
   832     by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v mem_cball)
   833 qed
   834 
   835 end