(* 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))" bundle lipschitz_syntax begin notation✐‹tag important› lipschitz_on ("_-lipschitz'_on" [1000]) end bundle no_lipschitz_syntax begin no_notation lipschitz_on ("_-lipschitz'_on" [1000]) end unbundle lipschitz_syntax lemma lipschitz_onI: "L-lipschitz_on X f" if "⋀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