Theory Lipschitz

(*  Title:      HOL/Analysis/Lipschitz.thy
    Author:     Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    Author:     Fabian Immler, TU München
*)
section ‹Lipschitz Continuity›

theory Lipschitz
  imports
    Derivative Abstract_Metric_Spaces
begin

definition✐‹tag important› lipschitz_on
  where "lipschitz_on C U f ⟷ (0 ≤ C ∧ (∀x ∈ U. ∀y∈U. dist (f x) (f y) ≤ C * dist x y))"

open_bundle lipschitz_syntax
begin
notation✐‹tag important›
  lipschitz_on (‹(‹open_block notation=‹postfix lipschitz_on››_-lipschitz'_on)› [1000])
end

lemma lipschitz_onI: "L-lipschitz_on X f"
  if "⋀x y. x ∈ X ⟹ y ∈ X ⟹ dist (f x) (f y) ≤ L * dist x y" "0 ≤ L"
  using that by (auto simp: lipschitz_on_def)

lemma lipschitz_onD:
  "dist (f x) (f y) ≤ L * dist x y"
  if "L-lipschitz_on X f" "x ∈ X" "y ∈ X"
  using that by (auto simp: lipschitz_on_def)

lemma lipschitz_on_nonneg:
  "0 ≤ L" if "L-lipschitz_on X f"
  using that by (auto simp: lipschitz_on_def)

lemma lipschitz_on_normD:
  "norm (f x - f y) ≤ L * norm (x - y)"
  if "lipschitz_on L X f" "x ∈ X" "y ∈ 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 ⊆ E" "M ≤ 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 "⋀x y. x ∈ X ⟹ y ∈ X ⟹ x ≤ y ⟹ dist (f x) (f y) ≤ L * dist x y"
    "0 ≤ L"
  for f::"'a::{linorder_topology, ordered_real_vector, metric_space} ⇒ 'b::metric_space"
proof (rule lipschitz_onI)
  fix x y assume xy: "x ∈ X" "y ∈ X"
  consider "y ≤ x" | "x ≤ y"
    by (rule le_cases)
  then show "dist (f x) (f y) ≤ L * dist x y"
  proof cases
    case 1
    then have "dist (f y) (f x) ≤ 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} (λx. if x ≤ b then f x else g x)"
    (is "lipschitz_on _ _ ?f")
proof (rule lipschitz_on_leI)
  fix x y
  assume x: "x ∈ {a..c}" and y: "y ∈ {a..c}" and xy: "x ≤ y"
  consider "x ≤ b ∧ b < y" | "x ≥ b ∨ y ≤ b" by arith
  then show "dist (?f x) (?f y) ≤ L * dist x y"
  proof cases
    case 1
    have "dist (f x) (g y) ≤ dist (f x) (f b) + dist (g b) (g y)"
      unfolding fg by (rule dist_triangle)
    also have "dist (f x) (f b) ≤ L * dist x b"
      using 1 x
      by (auto intro!: lipschitz_onD[OF f])
    also have "dist (g b) (g y) ≤ 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) ≤ L * dist x b + L * dist b y"
      by simp
    also have "… = 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])

lemma 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} (λx. if x ≤ 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

text ‹Equivalence between "abstract" and "type class" Lipschitz notions, 
for all types in the metric space class›
lemma Lipschitz_map_euclidean [simp]:
  "Lipschitz_continuous_map euclidean_metric euclidean_metric f
     ⟷ (∃B. lipschitz_on B UNIV f)"  (is "?lhs ⟷ ?rhs")
proof
  show "?lhs ⟹ ?rhs"
    by (force simp add: Lipschitz_continuous_map_pos lipschitz_on_def less_le_not_le)
  show "?rhs ⟹ ?lhs"                             
    by (auto simp: Lipschitz_continuous_map_def lipschitz_on_def)
qed

subsubsection ‹Continuity›

proposition 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 "∃d>0. ∀x∈X. ∀x'∈X. dist x' x < d ⟶ dist (f x') (f x) < e"
    using lipschitz_onD[OF l] lipschitz_on_nonneg[OF assms] ‹0 < e›
    by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps)
qed

proposition 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 ∈ X"
  using lipschitz_on_continuous_on[OF that(1)] that(2)
  by (auto simp: continuous_on_eq_continuous_within)

subsubsection ‹Differentiable functions›

proposition bounded_derivative_imp_lipschitz:
  assumes "⋀x. x ∈ X ⟹ (f has_derivative f' x) (at x within X)"
  assumes convex: "convex X"
  assumes "⋀x. x ∈ X ⟹ onorm (f' x) ≤ C" "0 ≤ C"
  shows "C-lipschitz_on X f"
proof (rule lipschitz_onI)
  show "⋀x y. x ∈ X ⟹ y ∈ X ⟹ dist (f x) (f y) ≤ C * dist x y"
    by (auto intro!: assms differentiable_bound[unfolded dist_norm[symmetric], OF convex])
qed fact


subsubsection✐‹tag unimportant› ‹Structural introduction rules›

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 ≥ 0" using lipschitz_on_nonneg[OF f] lipschitz_on_nonneg[OF g] by auto
  fix x y assume H: "x ∈ U" "y ∈ U"
  have "dist (g (f x)) (g (f y)) ≤ D * dist (f x) (f y)"
    apply (rule lipschitz_onD[OF g]) using H by auto
  also have "... ≤ 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 ∘ f) x) ((g ∘ f) y) ≤ D * C* dist x y"
    unfolding comp_def by (auto simp add: mult.commute)
qed

lemma lipschitz_on_compose2:
  "(D * C)-lipschitz_on U (λ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 ⟷ D-lipschitz_on V f"
  if "C = D" "U = V" "⋀x. x ∈ V ⟹ 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"
    "⋀x. x ∈ U ⟹ g x = f x"
  using that
  by simp

lemma lipschitz_on_empty_iff[simp]: "C-lipschitz_on {} f ⟷ C ≥ 0"
  by (auto simp: lipschitz_on_def)

lemma lipschitz_on_insert_iff[simp]:
  "C-lipschitz_on (insert y X) f ⟷
    C-lipschitz_on X f ∧ (∀x ∈ X. dist (f x) (f y) ≤ C * dist x y)"
  by (auto simp: lipschitz_on_def dist_commute)

lemma lipschitz_on_singleton [lipschitz_intros]: "C ≥ 0 ⟹ C-lipschitz_on {x} f"
  and lipschitz_on_empty [lipschitz_intros]: "C ≥ 0 ⟹ C-lipschitz_on {} f"
  by simp_all

lemma lipschitz_on_id [lipschitz_intros]: "1-lipschitz_on U (λx. x)"
  by (auto simp: lipschitz_on_def)

lemma lipschitz_on_constant [lipschitz_intros]: "0-lipschitz_on U (λx. c)"
  by (auto simp: lipschitz_on_def)

lemma lipschitz_on_add [lipschitz_intros]:
  fixes f::"'a::metric_space ⇒'b::real_normed_vector"
  assumes "C-lipschitz_on U f"
    "D-lipschitz_on U g"
  shows "(C+D)-lipschitz_on U (λx. f x + g x)"
proof (rule lipschitz_onI)
  show "C + D ≥ 0"
    using lipschitz_on_nonneg[OF assms(1)] lipschitz_on_nonneg[OF assms(2)] by auto
  fix x y assume H: "x ∈ U" "y ∈ U"
  have "dist (f x + g x) (f y + g y) ≤ dist (f x) (f y) + dist (g x) (g y)"
    by (simp add: dist_triangle_add)
  also have "... ≤ 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) ≤ (C+D) * dist x y" by (auto simp add: algebra_simps)
qed

lemma lipschitz_on_cmult [lipschitz_intros]:
  fixes f::"'a::metric_space ⇒ 'b::real_normed_vector"
  assumes "C-lipschitz_on U f"
  shows "(abs(a) * C)-lipschitz_on U (λx. a *⇩R f x)"
proof (rule lipschitz_onI)
  show "abs(a) * C ≥ 0" using lipschitz_on_nonneg[OF assms(1)] by auto
  fix x y assume H: "x ∈ U" "y ∈ U"
  have "dist (a *⇩R f x) (a *⇩R f y) = abs(a) * dist (f x) (f y)"
    by (metis dist_norm norm_scaleR real_vector.scale_right_diff_distrib)
  also have "... ≤ 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 *⇩R f x) (a *⇩R f y) ≤ ¦a¦ * C * dist x y" by auto
qed

lemma lipschitz_on_cmult_real [lipschitz_intros]:
  fixes f::"'a::metric_space ⇒ real"
  assumes "C-lipschitz_on U f"
  shows "(abs(a) * C)-lipschitz_on U (λx. a * f x)"
  using lipschitz_on_cmult[OF assms] by auto

lemma lipschitz_on_cmult_nonneg [lipschitz_intros]:
  fixes f::"'a::metric_space ⇒ 'b::real_normed_vector"
  assumes "C-lipschitz_on U f"
    "a ≥ 0"
  shows "(a * C)-lipschitz_on U (λx. a *⇩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 ⇒ real"
  assumes "C-lipschitz_on U f"
    "a ≥ 0"
  shows "(a * C)-lipschitz_on U (λ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 ⇒ 'b::real_normed_vector"
  assumes "C-lipschitz_on U f"
    "abs(a) ≤ D"
  shows "(D * C)-lipschitz_on U (λx. a *⇩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 ⇒ real"
  assumes "C-lipschitz_on U f"
    "abs(a) ≤ D"
  shows "(D * C)-lipschitz_on U (λx. a * f x)"
  using lipschitz_on_cmult_upper[OF assms] by auto

lemma lipschitz_on_minus[lipschitz_intros]:
  fixes f::"'a::metric_space ⇒'b::real_normed_vector"
  assumes "C-lipschitz_on U f"
  shows "C-lipschitz_on U (λx. - f x)"
  by (metis (mono_tags, lifting) assms dist_minus lipschitz_on_def)

lemma lipschitz_on_minus_iff[simp]:
  "L-lipschitz_on X (λx. - f x) ⟷ L-lipschitz_on X f"
  "L-lipschitz_on X (- f) ⟷ L-lipschitz_on X f"
  for f::"'a::metric_space ⇒'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 ⇒'b::real_normed_vector"
  assumes "C-lipschitz_on U f" "D-lipschitz_on U g"
  shows "(C + D)-lipschitz_on U (λ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 ≥ 0" using lipschitz_on_nonneg[OF assms(1)] by simp
  fix x y assume "x ∈ closure U" "y ∈ closure U"
  obtain u v::"nat ⇒ 'a" where *: "⋀n. u n ∈ U" "u ⇢ x"
                                   "⋀n. v n ∈ U" "v ⇢ y"
    using ‹x ∈ closure U› ‹y ∈ closure U› unfolding closure_sequential by blast
  have a: "(λn. f (u n)) ⇢ f x"
    using *(1) *(2) ‹x ∈ closure U› ‹continuous_on (closure U) f›
    unfolding comp_def continuous_on_closure_sequentially[of U f] by auto
  have b: "(λn. f (v n)) ⇢ f y"
    using *(3) *(4) ‹y ∈ closure U› ‹continuous_on (closure U) f›
    unfolding comp_def continuous_on_closure_sequentially[of U f] by auto
  have l: "(λn. C * dist (u n) (v n) - dist (f (u n)) (f (v n))) ⇢ 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)) ≥ 0" for n
    using lipschitz_onD(1)[OF assms(1) ‹u n ∈ U› ‹v n ∈ U›] by simp
  then have "C * dist x y - dist (f x) (f y) ≥ 0" using LIMSEQ_le_const[OF l, of 0] by auto
  then show "dist (f x) (f y) ≤ 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⇧2 + M⇧2))-lipschitz_on A (λ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))⇧2 + (dist (g x) (g y))⇧2)"
    by (auto simp add: dist_Pair_Pair real_le_lsqrt)
  also have "… ≤ sqrt ((L * dist x y)⇧2 + (M * dist x y)⇧2)"
    by (auto intro!: real_sqrt_le_mono add_mono power_mono 1 lipschitz_onD f g)
  also have "… ≤ sqrt (L⇧2 + M⇧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) ⇒ ('b::complete_space)"
  assumes "C-lipschitz_on U f"
  shows "∃g. C-lipschitz_on (closure U) g ∧ (∀x∈U. g x = f x)"
proof -
  obtain g where g: "⋀x. x ∈ U ⟹ 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 ≥ 0" "⋀x. norm (f x) ≤ 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 ‹Local Lipschitz continuity›

text ‹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.›

lemma locally_lipschitz_imp_lipschitz_aux:
  fixes f::"real ⇒ ('a::metric_space)"
  assumes "a ≤ b"
          "continuous_on {a..b} f"
          "⋀x. x ∈ {a..<b} ⟹ ∃y ∈ {x<..b}. dist (f y) (f x) ≤ M * (y-x)"
  shows "dist (f b) (f a) ≤ M * (b-a)"
proof -
  define A where "A = {x ∈ {a..b}. dist (f x) (f a) ≤ M * (x-a)}"
  have *: "A = (λx. M * (x-a) - dist (f x) (f a))-`{0..} ∩ {a..b}"
    unfolding A_def by auto
  have "a ∈ A" unfolding A_def using ‹a ≤ b› by auto
  then have "A ≠ {}" 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 ∈ A" by (rule closed_contains_Sup)
  have "Sup A = b"
  proof (rule ccontr)
    assume "Sup A ≠ b"
    define x where "x = Sup A"
    have I: "dist (f x) (f a) ≤ M * (x-a)" using ‹Sup A ∈ A› x_def A_def by auto
    have "x ∈ {a..<b}" unfolding x_def using ‹Sup A ∈ A› ‹Sup A ≠ b› A_def by auto
    then obtain y where J: "y ∈ {x<..b}" "dist (f y) (f x) ≤ M * (y-x)" using assms(3) by blast
    have "dist (f y) (f a) ≤ dist (f y) (f x) + dist (f x) (f a)" by (rule dist_triangle)
    also have "... ≤ M * (y-x) + M * (x-a)" using I J(2) by auto
    finally have "dist (f y) (f a) ≤ M * (y-a)" by (auto simp add: algebra_simps)
    then have "y ∈ A" unfolding A_def using ‹y ∈ {x<..b}› ‹x ∈ {a..<b}› by auto
    then have "y ≤ Sup A" by (rule cSup_upper, auto simp: A_def)
    then show False using ‹y ∈ {x<..b}› x_def by auto
  qed
  then show ?thesis using ‹Sup A ∈ A› A_def by auto
qed

lemma locally_lipschitz_imp_lipschitz:
  fixes f::"real ⇒ ('a::metric_space)"
  assumes "continuous_on {a..b} f"
          "⋀x y. x ∈ {a..<b} ⟹ y > x ⟹ ∃z ∈ {x<..y}. dist (f z) (f x) ≤ M * (z-x)"
          "M ≥ 0"
  shows "lipschitz_on M {a..b} f"
proof (rule lipschitz_onI[OF _ ‹M ≥ 0›])
  have *: "dist (f t) (f s) ≤ M * (t-s)" if "s ≤ t" "s ∈ {a..b}" "t ∈ {a..b}" for s t
  proof (rule locally_lipschitz_imp_lipschitz_aux, simp add: ‹s ≤ t›)
    show "continuous_on {s..t} f" using continuous_on_subset[OF assms(1)] that by auto
    fix x assume "x ∈ {s..<t}"
    then have "x ∈ {a..<b}" using that by auto
    show "∃z∈{x<..t}. dist (f z) (f x) ≤ M * (z - x)"
      using assms(2)[OF ‹x ∈ {a..<b}›, of t] ‹x ∈ {s..<t}› by auto
  qed
  fix x y assume "x ∈ {a..b}" "y ∈ {a..b}"
  consider "x ≤ y" | "y ≤ x" by linarith
  then show "dist (f x) (f y) ≤ M * dist x y"
    apply (cases)
    using *[OF _ ‹x ∈ {a..b}› ‹y ∈ {a..b}›] *[OF _ ‹y ∈ {a..b}› ‹x ∈ {a..b}›]
    by (auto simp add: dist_commute dist_real_def)
qed

text ‹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.›

proposition lipschitz_on_closed_Union:
  assumes "⋀i. i ∈ I ⟹ lipschitz_on M (U i) f"
          "⋀i. i ∈ I ⟹ closed (U i)"
          "finite I"
          "M ≥ 0"
          "{u..(v::real)} ⊆ (⋃i∈I. U i)"
  shows "lipschitz_on M {u..v} f"
proof (rule locally_lipschitz_imp_lipschitz[OF _ _ ‹M ≥ 0›])
  have *: "continuous_on (U i) f" if "i ∈ I" for i
    by (rule lipschitz_on_continuous_on[OF assms(1)[OF ‹i∈ I›]])
  have "continuous_on (⋃i∈I. U i) f"
    apply (rule continuous_on_closed_Union) using ‹finite I› * assms(2) by auto
  then show "continuous_on {u..v} f"
    using ‹{u..(v::real)} ⊆ (⋃i∈I. U i)› continuous_on_subset by auto

  fix z Z assume z: "z ∈ {u..<v}" "z < Z"
  then have "u ≤ v" by auto
  define T where "T = min Z v"
  then have T: "T > z" "T ≤ v" "T ≥ u" "T ≤ Z" using z by auto
  define A where "A = (⋃i∈ I ∩ {i. U i ∩ {z<..T} ≠ {}}. U i ∩ {z..T})"
  have a: "closed A"
    unfolding A_def apply (rule closed_UN) using ‹finite I› ‹⋀i. i ∈ I ⟹ closed (U i)› by auto
  have b: "bdd_below A" unfolding A_def using ‹finite I› by auto
  have "∃i ∈ I. T ∈ U i" using ‹{u..v} ⊆ (⋃i∈I. U i)› T by auto
  then have c: "T ∈ A" unfolding A_def using T by (auto, fastforce)
  have "Inf A ≥ z"
    apply (rule cInf_greatest, auto) using c unfolding A_def by auto
  moreover have "Inf A ≤ z"
  proof (rule ccontr)
    assume "¬(Inf A ≤ z)"
    then obtain w where w: "w > z" "w < Inf A" by (meson dense not_le_imp_less)
    have "Inf A ≤ T" using a b c by (simp add: cInf_lower)
    then have "w ≤ T" using w by auto
    then have "w ∈ {u..v}" using w ‹z ∈ {u..<v}› T by auto
    then obtain j where j: "j ∈ I" "w ∈ U j" using ‹{u..v} ⊆ (⋃i∈I. U i)› by fastforce
    then have "w ∈ U j ∩ {z..T}" "U j ∩ {z<..T} ≠ {}" using j T w ‹w ≤ T› by auto
    then have "w ∈ A" unfolding A_def using ‹j ∈ I› by auto
    then have "Inf A ≤ 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 ∈ A"
    apply (rule closed_contains_Inf) using a b c by auto
  ultimately have "z ∈ A" by simp
  then obtain i where i: "i ∈ I" "U i ∩ {z<..T} ≠ {}" "z ∈ U i" unfolding A_def by auto
  then obtain t where "t ∈ U i ∩ {z<..T}" by blast
  then have "dist (f t) (f z) ≤ M * (t - z)"
    using lipschitz_onD(1)[OF assms(1)[of i], of t z] i dist_real_def by auto
  then show "∃t∈{z<..Z}. dist (f t) (f z) ≤ M * (t - z)" using ‹T ≤ Z› ‹t ∈ U i ∩ {z<..T}› by auto
qed


subsection ‹Local Lipschitz continuity (uniform for a family of functions)›

definition✐‹tag important› local_lipschitz::
  "'a::metric_space set ⇒ 'b::metric_space set ⇒ ('a ⇒ 'b ⇒ 'c::metric_space) ⇒ bool"
  where
  "local_lipschitz T X f ≡ ∀x ∈ X. ∀t ∈ T.
    ∃u>0. ∃L. ∀t ∈ cball t u ∩ T. L-lipschitz_on (cball x u ∩ X) (f t)"

lemma local_lipschitzI:
  assumes "⋀t x. t ∈ T ⟹ x ∈ X ⟹ ∃u>0. ∃L. ∀t ∈ cball t u ∩ T. L-lipschitz_on (cball x u ∩ 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 ∈ T" "x ∈ X"
  obtains u L where "u > 0" "⋀s. s ∈ cball t u ∩ T ⟹ L-lipschitz_on (cball x u ∩ 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 ∈ T"
  shows "continuous_on X (f t)"
  unfolding continuous_on_def
proof safe
  fix x assume "x ∈ X"
  from local_lipschitzE[OF local_lipschitz ‹t ∈ T› ‹x ∈ X›] obtain u L
    where "0 < u"
    and L: "⋀s. s ∈ cball t u ∩ T ⟹ L-lipschitz_on (cball x u ∩ X) (f s)"
    by metis
  have "x ∈ ball x u" using ‹0 < u› by simp
  from lipschitz_on_continuous_on[OF L]
  have tendsto: "(f t ⤏ f t x) (at x within cball x u ∩ X)"
    using ‹0 < u› ‹x ∈ X› ‹t ∈ T›
    by (auto simp: continuous_on_def)
  moreover have "∀⇩F xa in at x. (xa ∈ cball x u ∩ X) = (xa ∈ X)"
    using eventually_at_ball[OF ‹0 < u›, of x UNIV]
    by eventually_elim auto
  ultimately show "(f t ⤏ 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 (λt. f t)"
  assumes g: "continuous_on T g"
  shows "local_lipschitz T X (λt. f (g t))"
proof (rule local_lipschitzI)
  fix t x
  assume "t ∈ T" "x ∈ X"
  then have "g t ∈ g ` T" by simp
  from local_lipschitzE[OF assms(1) this ‹x ∈ X›]
  obtain u L where "0 < u" and l: "(⋀s. s ∈ cball (g t) u ∩ g ` T ⟹ L-lipschitz_on (cball x u ∩ X) (f s))"
    by auto
  from g[unfolded continuous_on_eq_continuous_within, rule_format, OF ‹t ∈ T›,
    unfolded continuous_within_eps_delta, rule_format, OF ‹0 < u›]
  obtain d where d: "d>0" "⋀x'. x'∈T ⟹ dist x' t < d ⟹ dist (g x') (g t) < u"
    by (auto)
  show "∃u>0. ∃L. ∀t∈cball t u ∩ T. L-lipschitz_on  (cball x u ∩ X) (f (g t))"
    using d ‹0 < u›
    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)
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: "⋀x. x ∈ X ⟹ continuous_on T (λt. f t x)"
  shows "continuous_on (T × X) (λ(t, x). f t x)"
  unfolding continuous_on_iff
proof (safe, simp)
  fix a b and e::real
  assume H: "a ∈ T" "b ∈ X" "0 < e"
  hence "0 < e/2" by simp
  from y[unfolded continuous_on_iff, OF ‹b ∈ X›, rule_format, OF ‹a ∈ T› ‹0 < e/2›]
  obtain d where d: "d > 0" "⋀t. t ∈ T ⟹ dist t a < d ⟹ dist (f t b) (f a b) < e/2"
    by auto

  from ‹a : T› ‹b ∈ X›
  obtain u L where u: "0 < u"
    and L: "⋀t. t ∈ cball a u ∩ T ⟹ L-lipschitz_on  (cball b u ∩ X) (f t)"
    by (erule local_lipschitzE[OF local_lipschitz])

  have "a ∈ cball a u ∩ T" by (auto simp: ‹0 < u› ‹a ∈ T› less_imp_le)
  from lipschitz_on_nonneg[OF L[OF ‹a ∈ cball _ _ ∩ _›]] have "0 ≤ L" .

  let ?d = "Min {d, u, (e/2/(L + 1))}"
  show "∃d>0. ∀x∈T. ∀y∈X. dist (x, y) (a, b) < d ⟶ dist (f x y) (f a b) < e"
  proof (rule exI[where x = ?d], safe)
    show "0 < ?d"
      using ‹0 ≤ L› ‹0 < u› ‹0 < e› ‹0 < d›
      by (auto intro!: divide_pos_pos )
    fix x y
    assume "x ∈ T" "y ∈ X"
    assume dist_less: "dist (x, y) (a, b) < ?d"
    have "dist y b ≤ 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 ≤ u" by simp
      finally have "dist y b < u" .
    }
    have "?d ≤ e/2/(L + 1)" by simp
    also have "(L + 1) * … ≤ e / 2"
      using ‹0 < e› ‹L ≥ 0›
      by (auto simp: field_split_simps)
    finally have le1: "(L + 1) * dist y b < e / 2" using ‹L ≥ 0› by simp

    have "dist x a ≤ 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 ≤ d" by simp
    finally have "dist x a < d" .
    note ‹dist x a < ?d›
    also have "?d ≤ u" by simp
    finally have "dist x a < u" .
    then have "x ∈ cball a u ∩ T"
      using ‹x ∈ T›
      by (auto simp: dist_commute)
    have "dist (f x y) (f a b) ≤ 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 ∩ X) (f x)"
      using L[OF ‹x ∈ cball a u ∩ T›]
      by (rule lipschitz_on_le) simp
    then have "dist (f x y) (f x b) ≤ (L + 1) * dist y b"
      apply (rule lipschitz_onD)
      subgoal
        using ‹y ∈ X› ‹dist y b < u›
        by (simp add: dist_commute)
      subgoal
        using ‹0 < u› ‹b ∈ X›
        by simp
      done
    also have "(L + 1) * dist y b ≤ e / 2"
      using le1 ‹0 ≤ L› 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: "⋀x. x ∈ X ⟹ continuous_on T (λt. f t x)"
  obtains L where "⋀t. t ∈ T ⟹ L-lipschitz_on X (f t)"
proof -
  {
    assume *: "⋀n::nat. ¬(∀t∈T. n-lipschitz_on X (f t))"
    {
      fix n::nat
      from *[of n] have "∃x y t. t ∈ T ∧ x ∈ X ∧ y ∈ X ∧ dist (f t y) (f t x) > n * dist y x"
        by (force simp: lipschitz_on_def)
    } then obtain t and x y::"nat ⇒ 'b" where xy: "⋀n. x n ∈ X" "⋀n. y n ∈ X"
      and t: "⋀n. t n ∈ T"
      and d: "⋀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 ∈ X" "strict_mono (rx :: nat ⇒ nat)" "(x o rx) ⇢ lx"
      by (metis compact_def)
    with xy have "⋀n. (y o rx) n ∈ X" by auto
    with assms obtain ly ry where ly': "ly ∈ X" "strict_mono (ry :: nat ⇒ nat)" "((y o rx) o ry) ⇢ ly"
      by (metis compact_def)
    with t have "⋀n. ((t o rx) o ry) n ∈ T" by simp
    with assms obtain lt rt where lt': "lt ∈ T" "strict_mono (rt :: nat ⇒ nat)" "(((t o rx) o ry) o rt) ⇢ lt"
      by (metis compact_def)
    from lx' ly'
    have lx: "(x o (rx o ry o rt)) ⇢ lx" (is "?x ⇢ _")
      and ly: "(y o (rx o ry o rt)) ⇢ ly" (is "?y ⇢ _")
      and lt: "(t o (rx o ry o rt)) ⇢ lt" (is "?t ⇢ _")
      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 "(λn. dist (?y n) (?x n)) ⇢ dist ly lx"
      by (metis tendsto_dist)
    moreover
    let ?S = "(λ(t, x). f t x) ` (T × X)"
    have "eventually (λn::nat. n > 0) sequentially"
      by (metis eventually_at_top_dense)
    hence "eventually (λn. norm (dist (?y n) (?x n)) ≤ norm (¦diameter ?S¦ / n) * 1) sequentially"
    proof eventually_elim
      case (elim n)
      have "0 < rx (ry (rt n))" using ‹0 < n›
        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 ‹compact X› ‹compact T› 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 "… < dist (f (?t n) (?y n)) (f (?t n) (?x n)) / rx (ry (rt (n)))"
        using lx'(2) ly'(2) lt'(2) ‹0 < rx _›
        by (auto simp add: field_split_simps strict_mono_def)
      also have "… ≤ diameter ?S / n"
      proof (rule frac_le)
        show "diameter ?S ≥ 0"
          using compact compact_imp_bounded diameter_ge_0 by blast
        show "dist (f (?t n) (?y n)) (f (?t n) (?x n)) ≤ diameter ((λ(t,x). f t x) ` (T × X))"
          by (metis (no_types) compact compact_imp_bounded diameter_bounded_bound image_eqI mem_Sigma_iff o_apply split_conv t xy(1) xy(2))
        show "real n ≤ real (rx (ry (rt n)))"
          by (meson le_trans lt'(2) lx'(2) ly'(2) of_nat_mono strict_mono_imp_increasing)
      qed (use ‹n > 0› in auto)
      also have "… ≤ abs (diameter ?S) / n"
        by (auto intro!: divide_right_mono)
      finally show ?case by simp
    qed
    with _ have "(λn. dist (?y n) (?x n)) ⇢ 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 ∈ X" by auto
    from ‹lt ∈ T› this obtain u L where L: "u > 0" "⋀t. t ∈ cball lt u ∩ T ⟹ L-lipschitz_on (cball lx u ∩ X) (f t)"
      by (erule local_lipschitzE[OF local_lipschitz])
    hence "L ≥ 0" by (force intro!: lipschitz_on_nonneg ‹lt ∈ T›)

    from L lt ly lx ‹lx = ly›
    have
      "eventually (λn. ?t n ∈ ball lt u) sequentially"
      "eventually (λn. ?y n ∈ ball lx u) sequentially"
      "eventually (λn. ?x n ∈ ball lx u) sequentially"
      by (auto simp: dist_commute Lim)
    moreover have "eventually (λn. n > L) sequentially"
      by (metis filterlim_at_top_dense filterlim_real_sequentially)
    ultimately
    have "eventually (λ_. False) sequentially"
    proof eventually_elim
      case (elim n)
      hence "dist (f (?t n) (?y n)) (f (?t n) (?x n)) ≤ L * dist (?y n) (?x n)"
        using assms xy t
        unfolding dist_norm[symmetric]
        by (intro lipschitz_onD[OF L(2)]) (auto)
      also have "… ≤ n * dist (?y n) (?x n)"
        using elim by (intro mult_right_mono) auto
      also have "… ≤ 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 "… < 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 "⋀t. t ∈ T ⟹ L-lipschitz_on X (f t)"
    by metis
  thus ?thesis ..
qed

lemma local_lipschitz_subset:
  assumes "S ⊆ T" "Y ⊆ X"
  shows "local_lipschitz S Y f"
proof (rule local_lipschitzI)
  fix t x assume "t ∈ S" "x ∈ Y"
  then have "t ∈ T" "x ∈ X" using assms by auto
  from local_lipschitzE[OF local_lipschitz, OF this]
  obtain u L where u: "0 < u" and L: "⋀s. s ∈ cball t u ∩ T ⟹ L-lipschitz_on (cball x u ∩ X) (f s)"
    by blast
  show "∃u>0. ∃L. ∀t∈cball t u ∩ S. L-lipschitz_on (cball x u ∩ 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 ‹Y ⊆ X›]] L)
qed

end

lemma local_lipschitz_minus:
  fixes f::"'a::metric_space ⇒ 'b::metric_space ⇒ 'c::real_normed_vector"
  shows "local_lipschitz T X (λ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 (λa b. f a b)"
  assumes g: "local_lipschitz A B (λa b. g a b)"
  shows "local_lipschitz A B (λa b. (f a b, g a b))"
proof (rule local_lipschitzI)
  fix t x assume "t ∈ A" "x ∈ B"
  from local_lipschitzE[OF f this] local_lipschitzE[OF g this]
  obtain u L v M where "0 < u" "(⋀s. s ∈ cball t u ∩ A ⟹ L-lipschitz_on (cball x u ∩ B) (f s))"
    "0 < v" "(⋀s. s ∈ cball t v ∩ A ⟹ M-lipschitz_on (cball x v ∩ B) (g s))"
    by metis
  then show "∃u>0. ∃L. ∀t∈cball t u ∩ A. L-lipschitz_on (cball x u ∩ B) (λb. (f t b, g t b))"
    by (intro exI[where x="min u v"])
      (force intro: lipschitz_on_subset intro!: lipschitz_on_Pair)
qed

lemma local_lipschitz_constI: "local_lipschitz S T (λ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 (λ_. f)"
proof (rule local_lipschitzI, goal_cases)
  case (1 t x)
  from lipschitz_boundE[of "(cball x 1 ∩ B)"] obtain C where "C-lipschitz_on (cball x 1 ∩ B) f" by auto
  then show ?case
    by (auto intro: exI[where x=1])
qed

proposition c1_implies_local_lipschitz:
  fixes T::"real set" and X::"'a::{banach,heine_borel} set"
    and f::"real ⇒ 'a ⇒ 'a"
  assumes f': "⋀t x. t ∈ T ⟹ x ∈ X ⟹ (f t has_derivative blinfun_apply (f' (t, x))) (at x)"
  assumes cont_f': "continuous_on (T × X) f'"
  assumes "open T"
  assumes "open X"
  shows "local_lipschitz T X f"
proof (rule local_lipschitzI)
  fix t x
  assume "t ∈ T" "x ∈ X"
  from open_contains_cball[THEN iffD1, OF ‹open X›, rule_format, OF ‹x ∈ X›]
  obtain u where u: "u > 0" "cball x u ⊆ X" by auto
  moreover
  from open_contains_cball[THEN iffD1, OF ‹open T›, rule_format, OF ‹t ∈ T›]
  obtain v where v: "v > 0" "cball t v ⊆ T" by auto
  ultimately
  have "compact (cball t v × cball x u)" "cball t v × cball x u ⊆ T × X"
    by (auto intro!: compact_Times)
  then have "compact (f' ` (cball t v × cball x u))"
    by (auto intro!: compact_continuous_image continuous_on_subset[OF cont_f'])
  then obtain B where B: "B > 0" "⋀s y. s ∈ cball t v ⟹ y ∈ cball x u ⟹ norm (f' (s, y)) ≤ B"
    by (auto dest!: compact_imp_bounded simp: bounded_pos)

  have lipschitz: "B-lipschitz_on (cball x (min u v) ∩ X) (f s)" if s: "s ∈ cball t v" for s
  proof -
    note s
    also note ‹cball t v ⊆ T›
    finally
    have deriv: "⋀y. y ∈ cball x u ⟹ (f s has_derivative blinfun_apply (f' (s, y))) (at y within cball x u)"
      using ‹_ ⊆ X›
      by (auto intro!: has_derivative_at_withinI[OF f'])
    have "norm (f s y - f s z) ≤ B * norm (y - z)"
      if "y ∈ cball x u" "z ∈ 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])
    then show ?thesis
      using ‹0 < B›
      by (auto intro!: lipschitz_onI simp: dist_norm)
  qed
  show "∃u>0. ∃L. ∀t∈cball t u ∩ T. L-lipschitz_on (cball x u ∩ X) (f t)"
    by (force intro: exI[where x="min u v"] exI[where x=B] intro!: lipschitz simp: u v)
qed

end