Theory HOL-Analysis.Lipschitz
section ‹Lipschitz Continuity›
theory Lipschitz
imports
Derivative Abstract_Metric_Spaces Brouwer_Fixpoint
begin
definition 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
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 ‹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 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
subsection ‹bilipschitz homeomorphism results›
proposition bilipschitz_homeomorphism_spherical_projection:
fixes S :: "'a::euclidean_space set"
assumes "convex S" "bounded S" "0 ∈ rel_interior S"
shows "∃g. homeomorphism (rel_frontier S) (sphere 0 1 ∩ affine hull S)
(λx. x /⇩R norm x) g ∧
(∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶
norm (x /⇩R norm x - y /⇩R norm y) ≤ B * norm (x - y)) ∧
(∃B. ∀x y. x ∈ sphere 0 1 ∩ affine hull S ⟶
y ∈ sphere 0 1 ∩ affine hull S ⟶
norm (g x - g y) ≤ B * norm (x - y))"
proof -
obtain B where B: "⋀x y. x ∈ rel_frontier S ⟹ y ∈ rel_frontier S ⟹
dist (x /⇩R norm x) (y /⇩R norm y) ≤ B * dist x y"
using lipschitz_convex_spherical_projection[OF assms(1,3)] by blast
obtain b where "b > 0" and b: "⋀x y. x ∈ rel_frontier S ⟹ y ∈ rel_frontier S ⟹
b * dist x y ≤ dist ((1 / norm x) *⇩R x) ((1 / norm y) *⇩R y)"
using inverse_lipschitz_convex_spherical_projection[OF assms] by blast
have cont: "continuous_on (rel_frontier S) (λx. x /⇩R norm x)"
proof -
have "0 ∉ rel_frontier S"
using assms(3) by (auto simp: rel_frontier_def)
then show ?thesis
using continuous_on_Borsuk_map[of 0 "rel_frontier S"] by simp
qed
have zero_in_s: "0 ∈ S"
using assms(3) rel_interior_subset by blast
have zero_aff: "0 ∈ affine hull S"
using zero_in_s hull_subset[of S affine] by blast
have aff_eq_span: "affine hull S = span S"
using affine_hull_span_0[OF zero_aff] .
have image_eq: "(λx. x /⇩R norm x) ` rel_frontier S = sphere 0 1 ∩ affine hull S"
proof (rule set_eqI, rule iffI)
fix u assume "u ∈ (λx. x /⇩R norm x) ` rel_frontier S"
then obtain x where x_rf: "x ∈ rel_frontier S" and u_eq: "u = x /⇩R norm x"
by auto
have "x ≠ 0"
using x_rf assms(3) by (auto simp: rel_frontier_def)
then have "norm u = 1"
by (simp add: u_eq)
moreover have "u ∈ affine hull S"
proof -
have "x ∈ affine hull S"
using x_rf rel_frontier_affine_hull by blast
then have "x ∈ span S" using aff_eq_span by simp
then have "inverse (norm x) *⇩R x ∈ span S"
by (rule subspace_mul[OF real_vector.subspace_span])
then show ?thesis
using aff_eq_span u_eq by (simp add: field_simps)
qed
ultimately show "u ∈ sphere 0 1 ∩ affine hull S"
by (simp add: sphere_def)
next
fix u assume u_in: "u ∈ sphere 0 1 ∩ affine hull S"
then have "norm u = 1" and "u ∈ affine hull S"
by (auto simp: sphere_def)
then have "u ≠ 0" by auto
have "0 + u ∈ affine hull S"
using ‹u ∈ affine hull S› by simp
from ray_to_rel_frontier[OF assms(2) assms(3) this ‹u ≠ 0›]
obtain d where "d > 0" and d_rf: "0 + d *⇩R u ∈ rel_frontier S"
by blast
then have du_rf: "d *⇩R u ∈ rel_frontier S" by simp
have "(d *⇩R u) /⇩R norm (d *⇩R u) = u"
using ‹d > 0› ‹norm u = 1› by (simp add: norm_scaleR)
then show "u ∈ (λx. x /⇩R norm x) ` rel_frontier S"
using du_rf by force
qed
have x_ne: "⋀x. x ∈ rel_frontier S ⟹ x ≠ 0"
using assms(3) by (auto simp: rel_frontier_def)
have inj: "inj_on (λx. x /⇩R norm x) (rel_frontier S)"
using ‹0 < b› b
by (smt (verit) dist_le_zero_iff divide_inverse inj_on_def mult_le_0_iff scaleR_scaleR)
have "compact (rel_frontier S)"
using compact_rel_frontier_bounded assms(2) by blast
then obtain g where homeo: "homeomorphism (rel_frontier S)
(sphere 0 1 ∩ affine hull S) (λx. x /⇩R norm x) g"
using homeomorphism_compact[OF _ cont image_eq inj] by blast
have lip_f: "∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶
norm (x /⇩R norm x - y /⇩R norm y) ≤ B * norm (x - y)"
by (metis B dist_norm)
have lip_g: "∃B. ∀x y. x ∈ sphere 0 1 ∩ affine hull S ⟶
y ∈ sphere 0 1 ∩ affine hull S ⟶
norm (g x - g y) ≤ B * norm (x - y)"
proof (intro exI allI impI)
fix u v assume uv: "u ∈ sphere 0 1 ∩ affine hull S"
"v ∈ sphere 0 1 ∩ affine hull S"
have u_img: "u ∈ (λx. x /⇩R norm x) ` rel_frontier S"
and v_img: "v ∈ (λx. x /⇩R norm x) ` rel_frontier S"
using uv image_eq by auto
have gu: "g u ∈ rel_frontier S" and gv: "g v ∈ rel_frontier S"
using homeomorphism_image2[OF homeo] uv by auto
have fu: "(g u) /⇩R norm (g u) = u" and fv: "(g v) /⇩R norm (g v) = v"
using homeomorphism_apply2[OF homeo uv(1)] homeomorphism_apply2[OF homeo uv(2)] by auto
have "b * dist (g u) (g v) ≤ dist ((1 / norm (g u)) *⇩R (g u)) ((1 / norm (g v)) *⇩R (g v))"
using b[OF gu gv] .
also have "dist ((1 / norm (g u)) *⇩R (g u)) ((1 / norm (g v)) *⇩R (g v)) = dist u v"
using fu fv by (simp add: field_simps)
finally have "b * dist (g u) (g v) ≤ dist u v" .
then have "dist (g u) (g v) ≤ (1/b) * dist u v"
using ‹b > 0› by (simp add: field_simps)
then show "norm (g u - g v) ≤ (1/b) * norm (u - v)"
by (simp add: dist_norm)
qed
show ?thesis
using homeo lip_f lip_g by blast
qed
lemma bilipschitz_homeomorphism_rel_frontiers_aux:
fixes S t :: "'a::euclidean_space set"
assumes "convex S" "bounded S" "convex t" "bounded t"
"0 ∈ rel_interior S" "0 ∈ rel_interior t"
"affine hull S = affine hull t"
shows "∃f g. homeomorphism (rel_frontier S) (rel_frontier t) f g ∧
(∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶
norm (f x - f y) ≤ B * norm (x - y)) ∧
(∃B. ∀x y. x ∈ rel_frontier t ⟶ y ∈ rel_frontier t ⟶
norm (g x - g y) ≤ B * norm (x - y))"
proof -
let ?n = "λx::'a. x /⇩R norm x"
obtain gs where homeo_s: "homeomorphism (rel_frontier S) (sphere 0 1 ∩ affine hull S) ?n gs"
and lip_ns: "∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶
norm (?n x - ?n y) ≤ B * norm (x - y)"
and lip_gs: "∃B. ∀x y. x ∈ sphere 0 1 ∩ affine hull S ⟶
y ∈ sphere 0 1 ∩ affine hull S ⟶
norm (gs x - gs y) ≤ B * norm (x - y)"
using bilipschitz_homeomorphism_spherical_projection[OF assms(1,2,5)] by blast
obtain gt where homeo_t: "homeomorphism (rel_frontier t) (sphere 0 1 ∩ affine hull t) ?n gt"
and lip_nt: "∃B. ∀x y. x ∈ rel_frontier t ⟶ y ∈ rel_frontier t ⟶
norm (?n x - ?n y) ≤ B * norm (x - y)"
and lip_gt: "∃B. ∀x y. x ∈ sphere 0 1 ∩ affine hull t ⟶
y ∈ sphere 0 1 ∩ affine hull t ⟶
norm (gt x - gt y) ≤ B * norm (x - y)"
using bilipschitz_homeomorphism_spherical_projection[OF assms(3,4,6)] by blast
have mid_eq: "sphere 0 1 ∩ affine hull S = sphere 0 1 ∩ affine hull t"
using assms(7) by simp
have homeo_t': "homeomorphism (sphere 0 1 ∩ affine hull S) (rel_frontier t) gt ?n"
using homeomorphism_symD[OF homeo_t] mid_eq by simp
have homeo_comp: "homeomorphism (rel_frontier S) (rel_frontier t) (gt ∘ ?n) (gs ∘ ?n)"
using homeomorphism_compose[OF homeo_s homeo_t'] by simp
have lip_f: "∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶
norm ((gt ∘ ?n) x - (gt ∘ ?n) y) ≤ B * norm (x - y)"
proof -
obtain Bn where Bn: "⋀x y. x ∈ rel_frontier S ⟹ y ∈ rel_frontier S ⟹
norm (?n x - ?n y) ≤ Bn * norm (x - y)"
using lip_ns by blast
obtain Bg where Bg: "⋀x y. x ∈ sphere 0 1 ∩ affine hull S ⟹
y ∈ sphere 0 1 ∩ affine hull S ⟹
norm (gt x - gt y) ≤ Bg * norm (x - y)"
using lip_gt mid_eq by auto
have img_s: "?n ` rel_frontier S = sphere 0 1 ∩ affine hull S"
using homeomorphism_image1[OF homeo_s] .
have lip_n: "(max Bn 0)-lipschitz_on (rel_frontier S) ?n"
proof (rule lipschitz_onI)
fix x y assume "x ∈ rel_frontier S" "y ∈ rel_frontier S"
then have "dist (?n x) (?n y) ≤ Bn * dist x y"
using Bn by (simp add: dist_norm)
also have "… ≤ max Bn 0 * dist x y"
by (intro mult_right_mono) auto
finally show "dist (?n x) (?n y) ≤ max Bn 0 * dist x y" .
qed simp
have lip_g: "(max Bg 0)-lipschitz_on (sphere 0 1 ∩ affine hull S) gt"
proof (rule lipschitz_onI)
fix x y assume "x ∈ sphere 0 1 ∩ affine hull S" "y ∈ sphere 0 1 ∩ affine hull S"
then have "dist (gt x) (gt y) ≤ Bg * dist x y"
using Bg by (simp add: dist_norm)
also have "… ≤ max Bg 0 * dist x y"
by (intro mult_right_mono) auto
finally show "dist (gt x) (gt y) ≤ max Bg 0 * dist x y" .
qed simp
have "?n ` rel_frontier S = sphere 0 1 ∩ affine hull S"
using img_s .
then have lip_comp: "(max Bg 0 * max Bn 0)-lipschitz_on (rel_frontier S) (gt ∘ ?n)"
using lipschitz_on_compose[OF lip_n lip_g[unfolded img_s[symmetric]]]
by (simp add: img_s)
show ?thesis
proof (intro exI allI impI)
fix x y assume "x ∈ rel_frontier S" "y ∈ rel_frontier S"
then show "norm ((gt ∘ ?n) x - (gt ∘ ?n) y) ≤ (max Bg 0 * max Bn 0) * norm (x - y)"
using lipschitz_onD[OF lip_comp] by (simp add: dist_norm)
qed
qed
have lip_g: "∃B. ∀x y. x ∈ rel_frontier t ⟶ y ∈ rel_frontier t ⟶
norm ((gs ∘ ?n) x - (gs ∘ ?n) y) ≤ B * norm (x - y)"
proof -
obtain Bn where Bn: "⋀x y. x ∈ rel_frontier t ⟹ y ∈ rel_frontier t ⟹
norm (?n x - ?n y) ≤ Bn * norm (x - y)"
using lip_nt by blast
obtain Bg where Bg: "⋀x y. x ∈ sphere 0 1 ∩ affine hull S ⟹
y ∈ sphere 0 1 ∩ affine hull S ⟹
norm (gs x - gs y) ≤ Bg * norm (x - y)"
using lip_gs by blast
have img_t: "?n ` rel_frontier t = sphere 0 1 ∩ affine hull t"
using homeomorphism_image1[OF homeo_t] .
have lip_n: "(max Bn 0)-lipschitz_on (rel_frontier t) ?n"
proof (rule lipschitz_onI)
fix x y assume "x ∈ rel_frontier t" "y ∈ rel_frontier t"
then have "dist (?n x) (?n y) ≤ Bn * dist x y"
using Bn by (simp add: dist_norm)
also have "… ≤ max Bn 0 * dist x y"
by (intro mult_right_mono) auto
finally show "dist (?n x) (?n y) ≤ max Bn 0 * dist x y" .
qed simp
have lip_gs': "(max Bg 0)-lipschitz_on (sphere 0 1 ∩ affine hull S) gs"
proof (rule lipschitz_onI)
fix x y assume "x ∈ sphere 0 1 ∩ affine hull S" "y ∈ sphere 0 1 ∩ affine hull S"
then have "dist (gs x) (gs y) ≤ Bg * dist x y"
using Bg by (simp add: dist_norm)
also have "… ≤ max Bg 0 * dist x y"
by (intro mult_right_mono) auto
finally show "dist (gs x) (gs y) ≤ max Bg 0 * dist x y" .
qed simp
have lip_comp: "(max Bg 0 * max Bn 0)-lipschitz_on (rel_frontier t) (gs ∘ ?n)"
using lipschitz_on_compose[OF lip_n lip_gs'[unfolded mid_eq img_t[symmetric]]]
by simp
show ?thesis
proof (intro exI allI impI)
fix x y assume "x ∈ rel_frontier t" "y ∈ rel_frontier t"
then show "norm ((gs ∘ ?n) x - (gs ∘ ?n) y) ≤ (max Bg 0 * max Bn 0) * norm (x - y)"
using lipschitz_onD[OF lip_comp] by (simp add: dist_norm)
qed
qed
show ?thesis
using homeo_comp lip_f lip_g by blast
qed
lemma bilipschitz_homeomorphism_rel_frontiers_aux2:
fixes S :: "'a::euclidean_space set" and t :: "'b::euclidean_space set"
assumes "convex S" "bounded S" "convex t" "bounded t"
and "0 ∈ rel_interior S"
and "0 ∈ rel_interior t"
and "dim S = dim t"
obtains f g where "homeomorphism (rel_frontier S) (rel_frontier t) f g"
"∃B. ∀x∈rel_frontier S. ∀y∈rel_frontier S.
norm (f x - f y) ≤ B * norm (x - y)"
"∃B. ∀x∈rel_frontier t. ∀y∈rel_frontier t.
norm (g x - g y) ≤ B * norm (x - y)"
proof -
obtain h k where
lin_h: "linear h" and lin_k: "linear k"
and im_h: "h ` span S = span t" and im_k: "k ` span t = span S"
and norm_h: "⋀x. x ∈ span S ⟹ norm (h x) = norm x"
and norm_k: "⋀y. y ∈ span t ⟹ norm (k y) = norm y"
and kh: "⋀x. x ∈ span S ⟹ k (h x) = x"
and hk: "⋀y. y ∈ span t ⟹ h (k y) = y"
using isometries_subspaces [of "span S" "span t"] ‹dim S = dim t› by auto
have aff_h: "h ` (affine hull S) = affine hull t"
by (metis ‹0 ∈ rel_interior S› ‹0 ∈ rel_interior t› conic_hull_eq_span_affine_hull im_h)
have rel_frontier_h: "rel_frontier (h ` S) = h ` rel_frontier S"
proof -
have inj_h: "inj_on h (span S)"
using kh by (intro inj_onI) (metis)
have cls_span: "closure S ⊆ span S"
using closure_minimal [OF span_superset closed_span] by blast
have "rel_frontier (h ` S) = closure (h ` S) - rel_interior (h ` S)"
by (simp add: rel_frontier_def)
also have "closure (h ` S) = h ` closure S"
using closure_bounded_linear_image [OF lin_h ‹bounded S›] by simp
also have "rel_interior (h ` S) = h ` rel_interior S"
using rel_interior_convex_linear_image [OF lin_h ‹convex S›] by simp
also have "h ` closure S - h ` rel_interior S = h ` (closure S - rel_interior S)"
using inj_on_image_set_diff [OF inj_h]
cls_span rel_interior_subset [of S] span_superset [of S]
by (metis Diff_subset order_trans)
also have "closure S - rel_interior S = rel_frontier S"
by (simp add: rel_frontier_def)
finally show ?thesis .
qed
have aff_hs: "affine hull (h ` S) = affine hull t"
by (metis affine_hull_span_0 ‹0 ∈ rel_interior S› ‹0 ∈ rel_interior t› hull_inc im_h lin_h
linear_0 linear_span_image mem_rel_interior_ball rev_image_eqI)
have bdd_hs: "bounded (h ` S)"
using bounded_linear_image[OF ‹bounded S›] lin_h linear_linear by blast
have ri_hs: "0 ∈ rel_interior (h ` S)"
using rel_interior_convex_linear_image[OF lin_h ‹convex S›] ‹0 ∈ rel_interior S›
linear_0[OF lin_h] by (metis image_eqI)
obtain f g where
homeo_fg: "homeomorphism (rel_frontier (h ` S)) (rel_frontier t) f g"
and lip_f: "∃B. ∀x y. x ∈ rel_frontier (h ` S) ⟶ y ∈ rel_frontier (h ` S) ⟶
norm (f x - f y) ≤ B * norm (x - y)"
and lip_g: "∃B. ∀x y. x ∈ rel_frontier t ⟶ y ∈ rel_frontier t ⟶
norm (g x - g y) ≤ B * norm (x - y)"
using bilipschitz_homeomorphism_rel_frontiers_aux
[OF convex_linear_image[OF lin_h ‹convex S›] bdd_hs
‹convex t› ‹bounded t› ri_hs ‹0 ∈ rel_interior t› aff_hs]
by blast
let ?f = "f o h"
let ?g = "k o g"
show thesis
proof
show "homeomorphism (rel_frontier S) (rel_frontier t) ?f ?g"
proof (rule homeomorphism_compose)
show "homeomorphism (rel_frontier S) (h ` rel_frontier S) h k"
proof (unfold homeomorphism_def, intro conjI ballI)
have rfs_span: "rel_frontier S ⊆ span S"
using rel_frontier_affine_hull affine_hull_subset_span order_trans by blast
show "h ` rel_frontier S = h ` rel_frontier S" by simp
show "continuous_on (rel_frontier S) h"
using lin_h linear_continuous_on by (metis linear_linear)
show "k ` h ` rel_frontier S = rel_frontier S"
using kh rfs_span by (force simp: image_comp)
show "continuous_on (h ` rel_frontier S) k"
using lin_k linear_continuous_on by (metis linear_linear)
next
fix x assume "x ∈ rel_frontier S"
then show "k (h x) = x" using kh rel_frontier_affine_hull affine_hull_subset_span by blast
next
fix y assume "y ∈ h ` rel_frontier S"
then obtain x where "x ∈ rel_frontier S" "y = h x" by auto
then have "x ∈ span S" using rel_frontier_affine_hull affine_hull_subset_span by blast
then have "h x ∈ span t" using im_h by blast
then show "h (k y) = y" using hk ‹y = h x› by auto
qed
next
show "homeomorphism (h ` rel_frontier S) (rel_frontier t) f g"
using homeo_fg rel_frontier_h by simp
qed
show "∃B. ∀x∈rel_frontier S. ∀y∈rel_frontier S. norm ((?f x::'b) - ?f y) ≤ B * norm (x - y)"
proof -
obtain B where B: "⋀x y. x ∈ rel_frontier (h ` S) ⟹ y ∈ rel_frontier (h ` S) ⟹
norm (f x - f y) ≤ B * norm (x - y)"
using lip_f by blast
have "∀x∈rel_frontier S. ∀y∈rel_frontier S. norm ((f ∘ h) x - (f ∘ h) y) ≤ B * norm (x - y)"
proof (intro ballI)
fix x y assume x: "x ∈ rel_frontier S" and y: "y ∈ rel_frontier S"
have hx: "h x ∈ rel_frontier (h ` S)" using x rel_frontier_h by auto
have hy: "h y ∈ rel_frontier (h ` S)" using y rel_frontier_h by auto
have xs: "x ∈ span S"
using ‹0 ∈ rel_interior S› conic_hull_eq_span_affine_hull rel_frontier_affine_hull x by fastforce
have ys: "y ∈ span S"
using affine_hull_subset_span closure_affine_hull rel_frontier_def y by fastforce
show "norm ((f ∘ h) x - (f ∘ h) y) ≤ B * norm (x - y)"
by (smt (verit) B comp_def hx hy lin_h linear_diff norm_h span_diff xs ys)
qed
then show ?thesis by auto
qed
show "∃B. ∀x∈rel_frontier t. ∀y∈rel_frontier t. norm ((?g x::'a) - ?g y) ≤ B * norm (x - y)"
proof -
obtain B where B: "⋀x y. x ∈ rel_frontier t ⟹ y ∈ rel_frontier t ⟹
norm (g x - g y) ≤ B * norm (x - y)"
using lip_g by blast
have g_in_span: "⋀x. x ∈ rel_frontier t ⟹ g x ∈ span t"
by (metis aff_hs affine_hull_span_0 homeo_fg homeomorphism_def hull_inc imageI
rel_frontier_affine_hull rel_interior_subset ri_hs subsetD)
then show ?thesis
by (metis (no_types, lifting) B comp_def g_in_span lin_k linear_diff norm_k span_diff)
qed
qed
qed
lemma bilipschitz_homeomorphism_rel_frontiers:
fixes S t :: "'a::euclidean_space set"
assumes "convex S" "bounded S" "convex t" "bounded t" and eq: "aff_dim S = aff_dim t"
obtains f g where "homeomorphism (rel_frontier S) (rel_frontier t) f g"
"∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶
norm (f x - f y) ≤ B * norm (x - y)"
"∃B. ∀x y. x ∈ rel_frontier t ⟶ y ∈ rel_frontier t ⟶
norm (g x - g y) ≤ B * norm (x - y)"
proof (cases "S={} ∨ t={}")
case True
then show ?thesis
by (metis that aff_dim_negative_iff eq empty_iff homeomorphism_empty rel_frontier_empty)
next
case False
obtain a b where a: "a ∈ rel_interior S" and b: "b ∈ rel_interior t"
using False rel_interior_eq_empty[OF ‹convex S›] rel_interior_eq_empty[OF ‹convex t›]
by blast
have dim_eq: "dim ((+) (-a) ` S) = dim ((+) (-b) ` t)"
by (metis a aff_dim_eq_dim eq b hull_inc mem_rel_interior_ball of_nat_eq_iff)
have ri_s: "0 ∈ rel_interior ((+) (-a) ` S)"
using a rel_interior_translation[of "-a" S] by (auto simp: image_iff)
have ri_t: "0 ∈ rel_interior ((+) (-b) ` t)"
using b rel_interior_translation[of "-b" t] by (auto simp: image_iff)
obtain f g where
homeo: "homeomorphism (rel_frontier ((+) (-a) ` S)) (rel_frontier ((+) (-b) ` t)) f g"
and lip_f: "∃B. ∀x∈rel_frontier ((+) (-a) ` S). ∀y∈rel_frontier ((+) (-a) ` S).
norm (f x - f y) ≤ B * norm (x - y)"
and lip_g: "∃B. ∀x∈rel_frontier ((+) (-b) ` t). ∀y∈rel_frontier ((+) (-b) ` t).
norm (g x - g y) ≤ B * norm (x - y)"
using bilipschitz_homeomorphism_rel_frontiers_aux2
[OF convex_translation[OF ‹convex S›] bounded_translation[OF ‹bounded S›]
convex_translation[OF ‹convex t›] bounded_translation[OF ‹bounded t›]
ri_s ri_t dim_eq]
by blast
have rfs: "rel_frontier ((+) (-a) ` S) = (+) (-a) ` rel_frontier S"
by (rule rel_frontier_translation)
have rft: "rel_frontier ((+) (-b) ` t) = (+) (-b) ` rel_frontier t"
by (rule rel_frontier_translation)
obtain B B' where
lip_fs: "⋀x y. x ∈ rel_frontier S ⟹ y ∈ rel_frontier S ⟹
norm (f (-a + x) - f (-a + y)) ≤ B * norm (x - y)"
and lip_gt: "⋀x y. x ∈ rel_frontier t ⟹ y ∈ rel_frontier t ⟹
norm (g (-b + x) - g (-b + y)) ≤ B' * norm (x - y)"
proof -
obtain B where B: "∀x∈rel_frontier ((+) (-a) ` S). ∀y∈rel_frontier ((+) (-a) ` S).
norm (f x - f y) ≤ B * norm (x - y)"
using lip_f by blast
obtain B' where B': "∀x∈rel_frontier ((+) (-b) ` t). ∀y∈rel_frontier ((+) (-b) ` t).
norm (g x - g y) ≤ B' * norm (x - y)"
using lip_g by blast
show thesis
proof
fix x y assume "x ∈ rel_frontier S" "y ∈ rel_frontier S"
then have xy: "-a + x ∈ rel_frontier ((+) (-a) ` S)" "-a + y ∈ rel_frontier ((+) (-a) ` S)"
unfolding rfs by (auto simp: image_iff)
then show "norm (f (-a + x) - f (-a + y)) ≤ B * norm (x - y)"
using bspec[OF bspec[OF B xy(1)] xy(2)] by simp
next
fix x y assume "x ∈ rel_frontier t" "y ∈ rel_frontier t"
then have xy: "-b + x ∈ rel_frontier ((+) (-b) ` t)" "-b + y ∈ rel_frontier ((+) (-b) ` t)"
unfolding rft by (auto simp: image_iff)
then show "norm (g (-b + x) - g (-b + y)) ≤ B' * norm (x - y)"
using bspec[OF bspec[OF B' xy(1)] xy(2)] by simp
qed
qed
let ?f = "λx. b + f (-a + x)"
let ?g = "λx. a + g (-b + x)"
show thesis
proof
show "homeomorphism (rel_frontier S) (rel_frontier t) ?f ?g"
proof -
note homeo_parts = homeo[unfolded homeomorphism_def rfs rft]
have cf: "continuous_on ((+) (-a) ` rel_frontier S) f"
using homeo_parts by blast
have cg: "continuous_on ((+) (-b) ` rel_frontier t) g"
using homeo_parts by blast
have gf0: "⋀x. x ∈ (+) (-a) ` rel_frontier S ⟹ g (f x) = x"
using homeo_parts by blast
have fg0: "⋀y. y ∈ (+) (-b) ` rel_frontier t ⟹ f (g y) = y"
using homeo_parts by blast
have gf: "⋀x. x ∈ rel_frontier S ⟹ ?g (?f x) = x"
using gf0[of "-a + _"] by (auto simp: algebra_simps image_iff)
have fg: "⋀y. y ∈ rel_frontier t ⟹ ?f (?g y) = y"
using fg0[of "-b + _"] by (auto simp: algebra_simps image_iff)
have im_f: "?f ` rel_frontier S = rel_frontier t"
by (metis homeo_parts image_image translation_galois)
have im_g: "?g ` rel_frontier t = rel_frontier S"
by (metis homeo_parts image_image translation_galois)
have cont_f: "continuous_on (rel_frontier S) ?f"
using continuous_on_compose[OF _ cf]
continuous_on_translation_eq[of _ "-a" id] continuous_on_translation_eq[of _ b "f ∘ (+) (-a)"]
by (simp add: o_def)
have cont_g: "continuous_on (rel_frontier t) ?g"
using continuous_on_compose[OF _ cg]
continuous_on_translation_eq[of _ "-b" id] continuous_on_translation_eq[of _ a "g ∘ (+) (-b)"]
by (simp add: o_def)
show ?thesis
unfolding homeomorphism_def
using gf fg im_f im_g cont_f cont_g by blast
qed
next
show "∃B. ∀x y. x ∈ rel_frontier S ⟶ y ∈ rel_frontier S ⟶ norm ((?f x::'a) - ?f y) ≤ B * norm (x - y)"
using lip_fs by (force simp: algebra_simps)
show "∃B. ∀x y. x ∈ rel_frontier t ⟶ y ∈ rel_frontier t ⟶ norm ((?g x::'a) - ?g y) ≤ B * norm (x - y)"
using lip_gt by (force simp: algebra_simps)
qed
qed
end