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