# mathlib3documentation

topology.metric_space.lipschitz

# Lipschitz continuous functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A map f : α → β between two (extended) metric spaces is called Lipschitz continuous with constant K ≥ 0 if for all x, y we have edist (f x) (f y) ≤ K * edist x y. For a metric space, the latter inequality is equivalent to dist (f x) (f y) ≤ K * dist x y. There is also a version asserting this inequality only for x and y in some set s.

In this file we provide various ways to prove that various combinations of Lipschitz continuous functions are Lipschitz continuous. We also prove that Lipschitz continuous functions are uniformly continuous.

## Main definitions and lemmas #

• lipschitz_with K f: states that f is Lipschitz with constant K : ℝ≥0
• lipschitz_on_with K f: states that f is Lipschitz with constant K : ℝ≥0 on a set s
• lipschitz_with.uniform_continuous: a Lipschitz function is uniformly continuous
• lipschitz_on_with.uniform_continuous_on: a function which is Lipschitz on a set is uniformly continuous on that set.

## Implementation notes #

The parameter K has type ℝ≥0. This way we avoid conjuction in the definition and have coercions both to ℝ and ℝ≥0∞. Constructors whose names end with ' take K : ℝ as an argument, and return lipschitz_with (real.to_nnreal K) f.

def lipschitz_with {α : Type u} {β : Type v} (K : nnreal) (f : α β) :
Prop

A function f is Lipschitz continuous with constant K ≥ 0 if for all x, y we have dist (f x) (f y) ≤ K * dist x y

Equations
theorem lipschitz_with_iff_dist_le_mul {α : Type u} {β : Type v} {K : nnreal} {f : α β} :
(x y : α), has_dist.dist (f x) (f y) K *
theorem lipschitz_with.of_dist_le_mul {α : Type u} {β : Type v} {K : nnreal} {f : α β} :
( (x y : α), has_dist.dist (f x) (f y) K * y)

Alias of the reverse direction of lipschitz_with_iff_dist_le_mul.

theorem lipschitz_with.dist_le_mul {α : Type u} {β : Type v} {K : nnreal} {f : α β} :
(x y : α), has_dist.dist (f x) (f y) K *

Alias of the forward direction of lipschitz_with_iff_dist_le_mul.

def lipschitz_on_with {α : Type u} {β : Type v} (K : nnreal) (f : α β) (s : set α) :
Prop

A function f is Lipschitz continuous with constant K ≥ 0 on s if for all x, y in s we have dist (f x) (f y) ≤ K * dist x y

Equations
@[simp]
theorem lipschitz_on_with_empty {α : Type u} {β : Type v} (K : nnreal) (f : α β) :
theorem lipschitz_on_with.mono {α : Type u} {β : Type v} {K : nnreal} {s t : set α} {f : α β} (hf : t) (h : s t) :
s
theorem lipschitz_on_with_iff_dist_le_mul {α : Type u} {β : Type v} {K : nnreal} {s : set α} {f : α β} :
s (x : α), x s (y : α), y s has_dist.dist (f x) (f y) K *
theorem lipschitz_on_with.dist_le_mul {α : Type u} {β : Type v} {K : nnreal} {s : set α} {f : α β} :
s (x : α), x s (y : α), y s has_dist.dist (f x) (f y) K *

Alias of the forward direction of lipschitz_on_with_iff_dist_le_mul.

theorem lipschitz_on_with.of_dist_le_mul {α : Type u} {β : Type v} {K : nnreal} {s : set α} {f : α β} :
( (x : α), x s (y : α), y s has_dist.dist (f x) (f y) K * y) s

Alias of the reverse direction of lipschitz_on_with_iff_dist_le_mul.

@[simp]
theorem lipschitz_on_univ {α : Type u} {β : Type v} {K : nnreal} {f : α β} :
theorem lipschitz_on_with_iff_restrict {α : Type u} {β : Type v} {K : nnreal} {f : α β} {s : set α} :
s (s.restrict f)
theorem lipschitz_on_with.to_restrict {α : Type u} {β : Type v} {K : nnreal} {f : α β} {s : set α} :
s (s.restrict f)

Alias of the forward direction of lipschitz_on_with_iff_restrict.

theorem maps_to.lipschitz_on_with_iff_restrict {α : Type u} {β : Type v} {K : nnreal} {f : α β} {s : set α} {t : set β} (h : s t) :
s t h)
theorem lipschitz_on_with.to_restrict_maps_to {α : Type u} {β : Type v} {K : nnreal} {f : α β} {s : set α} {t : set β} (h : s t) :
s t h)

Alias of the forward direction of maps_to.lipschitz_on_with_iff_restrict.

@[protected]
theorem lipschitz_with.lipschitz_on_with {α : Type u} {β : Type v} {K : nnreal} {f : α β} (h : f) (s : set α) :
s
theorem lipschitz_with.edist_le_mul {α : Type u} {β : Type v} {K : nnreal} {f : α β} (h : f) (x y : α) :
has_edist.edist (f x) (f y) K *
theorem lipschitz_with.edist_le_mul_of_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} {x y : α} {r : ennreal} (h : f) (hr : r) :
has_edist.edist (f x) (f y) K * r
theorem lipschitz_with.edist_lt_mul_of_lt {α : Type u} {β : Type v} {K : nnreal} {f : α β} {x y : α} {r : ennreal} (h : f) (hK : K 0) (hr : < r) :
has_edist.edist (f x) (f y) < K * r
theorem lipschitz_with.maps_to_emetric_closed_ball {α : Type u} {β : Type v} {K : nnreal} {f : α β} (h : f) (x : α) (r : ennreal) :
r) (emetric.closed_ball (f x) (K * r))
theorem lipschitz_with.maps_to_emetric_ball {α : Type u} {β : Type v} {K : nnreal} {f : α β} (h : f) (hK : K 0) (x : α) (r : ennreal) :
r) (emetric.ball (f x) (K * r))
theorem lipschitz_with.edist_lt_top {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) {x y : α} (h : ) :
has_edist.edist (f x) (f y) <
theorem lipschitz_with.mul_edist_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} (h : f) (x y : α) :
(K)⁻¹ * has_edist.edist (f x) (f y)
@[protected]
theorem lipschitz_with.of_edist_le {α : Type u} {β : Type v} {f : α β} (h : (x y : α), has_edist.edist (f x) (f y) ) :
@[protected]
theorem lipschitz_with.weaken {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) {K' : nnreal} (h : K K') :
f
theorem lipschitz_with.ediam_image_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) (s : set α) :
theorem lipschitz_with.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) {x y : α} {d : ennreal} (h : < d / K) :
has_edist.edist (f x) (f y) < d
@[protected]
theorem lipschitz_with.uniform_continuous {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) :

A Lipschitz function is uniformly continuous

@[protected]
theorem lipschitz_with.continuous {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) :

A Lipschitz function is continuous

@[protected]
theorem lipschitz_with.const {α : Type u} {β : Type v} (b : β) :
(λ (a : α), b)
@[protected]
theorem lipschitz_with.id {α : Type u}  :
@[protected]
theorem lipschitz_with.subtype_val {α : Type u} (s : set α) :
@[protected]
theorem lipschitz_with.subtype_coe {α : Type u} (s : set α) :
theorem lipschitz_with.subtype_mk {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) {p : β Prop} (hp : (x : α), p (f x)) :
(λ (x : α), f x, _⟩)
@[protected]
theorem lipschitz_with.eval {ι : Type x} {α : ι Type u} [Π (i : ι), pseudo_emetric_space (α i)] [fintype ι] (i : ι) :
@[protected]
theorem lipschitz_with.restrict {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) (s : set α) :
(s.restrict f)
@[protected]
theorem lipschitz_with.comp {α : Type u} {β : Type v} {γ : Type w} {Kf Kg : nnreal} {f : β γ} {g : α β} (hf : f) (hg : g) :
lipschitz_with (Kf * Kg) (f g)
theorem lipschitz_with.comp_lipschitz_on_with {α : Type u} {β : Type v} {γ : Type w} {Kf Kg : nnreal} {f : β γ} {g : α β} {s : set α} (hf : f) (hg : s) :
lipschitz_on_with (Kf * Kg) (f g) s
@[protected]
theorem lipschitz_with.prod_fst {α : Type u} {β : Type v}  :
@[protected]
theorem lipschitz_with.prod_snd {α : Type u} {β : Type v}  :
@[protected]
theorem lipschitz_with.prod {α : Type u} {β : Type v} {γ : Type w} {f : α β} {Kf : nnreal} (hf : f) {g : α γ} {Kg : nnreal} (hg : g) :
lipschitz_with Kg) (λ (x : α), (f x, g x))
@[protected]
theorem lipschitz_with.prod_mk_left {α : Type u} {β : Type v} (a : α) :
(prod.mk a)
@[protected]
theorem lipschitz_with.prod_mk_right {α : Type u} {β : Type v} (b : β) :
(λ (a : α), (a, b))
@[protected]
theorem lipschitz_with.uncurry {α : Type u} {β : Type v} {γ : Type w} {f : α β γ} {Kα Kβ : nnreal} (hα : (b : β), (λ (a : α), f a b)) (hβ : (a : α), (f a)) :
lipschitz_with (Kα + Kβ)
@[protected]
theorem lipschitz_with.iterate {α : Type u} {K : nnreal} {f : α α} (hf : f) (n : ) :
theorem lipschitz_with.edist_iterate_succ_le_geometric {α : Type u} {K : nnreal} {f : α α} (hf : f) (x : α) (n : ) :
has_edist.edist (f^[n] x) (f^[n + 1] x) (f x) * K ^ n
@[protected]
theorem lipschitz_with.mul {α : Type u} {f g : function.End α} {Kf Kg : nnreal} (hf : f) (hg : g) :
lipschitz_with (Kf * Kg) (f * g)
@[protected]
theorem lipschitz_with.list_prod {α : Type u} {ι : Type x} (f : ι ) (K : ι nnreal) (h : (i : ι), lipschitz_with (K i) (f i)) (l : list ι) :

The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous endomorphism.

@[protected]
theorem lipschitz_with.pow {α : Type u} {f : function.End α} {K : nnreal} (h : f) (n : ) :
lipschitz_with (K ^ n) (f ^ n)
@[protected]
theorem lipschitz_with.of_dist_le' {α : Type u} {β : Type v} {f : α β} {K : } (h : (x y : α), has_dist.dist (f x) (f y) K * ) :
@[protected]
theorem lipschitz_with.mk_one {α : Type u} {β : Type v} {f : α β} (h : (x y : α), has_dist.dist (f x) (f y) ) :
@[protected]
theorem lipschitz_with.of_le_add_mul' {α : Type u} {f : α } (K : ) (h : (x y : α), f x f y + K * ) :

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version doesn't assume 0≤K.

@[protected]
theorem lipschitz_with.of_le_add_mul {α : Type u} {f : α } (K : nnreal) (h : (x y : α), f x f y + K * ) :

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version assumes 0≤K.

@[protected]
theorem lipschitz_with.of_le_add {α : Type u} {f : α } (h : (x y : α), f x f y + ) :
@[protected]
theorem lipschitz_with.le_add_mul {α : Type u} {f : α } {K : nnreal} (h : f) (x y : α) :
f x f y + K *
@[protected]
theorem lipschitz_with.iff_le_add_mul {α : Type u} {f : α } {K : nnreal} :
(x y : α), f x f y + K *
theorem lipschitz_with.nndist_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) (x y : α) :
has_nndist.nndist (f x) (f y) K *
theorem lipschitz_with.dist_le_mul_of_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} {x y : α} {r : } (hf : f) (hr : r) :
has_dist.dist (f x) (f y) K * r
theorem lipschitz_with.maps_to_closed_ball {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) (x : α) (r : ) :
r) (metric.closed_ball (f x) (K * r))
theorem lipschitz_with.dist_lt_mul_of_lt {α : Type u} {β : Type v} {K : nnreal} {f : α β} {x y : α} {r : } (hf : f) (hK : K 0) (hr : < r) :
has_dist.dist (f x) (f y) < K * r
theorem lipschitz_with.maps_to_ball {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) (hK : K 0) (x : α) (r : ) :
r) (metric.ball (f x) (K * r))
def lipschitz_with.to_locally_bounded_map {α : Type u} {β : Type v} {K : nnreal} (f : α β) (hf : f) :

A Lipschitz continuous map is a locally bounded map.

Equations
@[simp]
theorem lipschitz_with.coe_to_locally_bounded_map {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) :
theorem lipschitz_with.comap_cobounded_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) :
theorem lipschitz_with.bounded_image {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) {s : set α} (hs : metric.bounded s) :
theorem lipschitz_with.diam_image_le {α : Type u} {β : Type v} {K : nnreal} {f : α β} (hf : f) (s : set α) (hs : metric.bounded s) :
@[protected]
theorem lipschitz_with.dist_left {α : Type u} (y : α) :
(λ (x : α), y)
@[protected]
theorem lipschitz_with.dist_right {α : Type u} (x : α) :
@[protected]
theorem lipschitz_with.dist {α : Type u}  :
theorem lipschitz_with.dist_iterate_succ_le_geometric {α : Type u} {K : nnreal} {f : α α} (hf : f) (x : α) (n : ) :
has_dist.dist (f^[n] x) (f^[n + 1] x) (f x) * K ^ n
theorem lipschitz_with_max  :
(λ (p : × ), p.snd)
theorem lipschitz_with_min  :
(λ (p : × ), p.snd)
@[protected]
theorem lipschitz_with.max {α : Type u} {f g : α } {Kf Kg : nnreal} (hf : f) (hg : g) :
lipschitz_with Kg) (λ (x : α), linear_order.max (f x) (g x))
@[protected]
theorem lipschitz_with.min {α : Type u} {f g : α } {Kf Kg : nnreal} (hf : f) (hg : g) :
lipschitz_with Kg) (λ (x : α), linear_order.min (f x) (g x))
theorem lipschitz_with.max_const {α : Type u} {f : α } {Kf : nnreal} (hf : f) (a : ) :
(λ (x : α), linear_order.max (f x) a)
theorem lipschitz_with.const_max {α : Type u} {f : α } {Kf : nnreal} (hf : f) (a : ) :
(λ (x : α), (f x))
theorem lipschitz_with.min_const {α : Type u} {f : α } {Kf : nnreal} (hf : f) (a : ) :
(λ (x : α), linear_order.min (f x) a)
theorem lipschitz_with.const_min {α : Type u} {f : α } {Kf : nnreal} (hf : f) (a : ) :
(λ (x : α), (f x))
@[protected]
theorem lipschitz_with.proj_Icc {a b : } (h : a b) :
b h)
theorem metric.bounded.left_of_prod {α : Type u} {β : Type v} {s : set α} {t : set β} (h : metric.bounded (s ×ˢ t)) (ht : t.nonempty) :
theorem metric.bounded.right_of_prod {α : Type u} {β : Type v} {s : set α} {t : set β} (h : metric.bounded (s ×ˢ t)) (hs : s.nonempty) :
theorem metric.bounded_prod_of_nonempty {α : Type u} {β : Type v} {s : set α} {t : set β} (hs : s.nonempty) (ht : t.nonempty) :
theorem metric.bounded_prod {α : Type u} {β : Type v} {s : set α} {t : set β} :
@[protected]
theorem lipschitz_on_with.uniform_continuous_on {α : Type u} {β : Type v} {K : nnreal} {s : set α} {f : α β} (hf : s) :
@[protected]
theorem lipschitz_on_with.continuous_on {α : Type u} {β : Type v} {K : nnreal} {s : set α} {f : α β} (hf : s) :
theorem lipschitz_on_with.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} {K : nnreal} {s : set α} {f : α β} (hf : s) {x y : α} (hx : x s) (hy : y s) {d : ennreal} (hd : < d / K) :
has_edist.edist (f x) (f y) < d
@[protected]
theorem lipschitz_on_with.comp {α : Type u} {β : Type v} {γ : Type w} {K : nnreal} {s : set α} {f : α β} {g : β γ} {t : set β} {Kg : nnreal} (hg : t) (hf : s) (hmaps : s t) :
lipschitz_on_with (Kg * K) (g f) s
theorem lipschitz_on_with.ediam_image2_le {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) {K₁ K₂ : nnreal} (s : set α) (t : set β) (hf₁ : (b : β), b t (λ (a : α), f a b) s) (hf₂ : (a : α), a s (f a) t) :
emetric.diam s t) K₁ * + K₂ *
@[protected]
theorem lipschitz_on_with.of_dist_le' {α : Type u} {β : Type v} {s : set α} {f : α β} {K : } (h : (x : α), x s (y : α), y s has_dist.dist (f x) (f y) K * ) :
@[protected]
theorem lipschitz_on_with.mk_one {α : Type u} {β : Type v} {s : set α} {f : α β} (h : (x : α), x s (y : α), y s has_dist.dist (f x) (f y) ) :
s
@[protected]
theorem lipschitz_on_with.of_le_add_mul' {α : Type u} {s : set α} {f : α } (K : ) (h : (x : α), x s (y : α), y s f x f y + K * ) :

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version doesn't assume 0≤K.

@[protected]
theorem lipschitz_on_with.of_le_add_mul {α : Type u} {s : set α} {f : α } (K : nnreal) (h : (x : α), x s (y : α), y s f x f y + K * ) :
s

For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version assumes 0≤K.

@[protected]
theorem lipschitz_on_with.of_le_add {α : Type u} {s : set α} {f : α } (h : (x : α), x s (y : α), y s f x f y + ) :
s
@[protected]
theorem lipschitz_on_with.le_add_mul {α : Type u} {s : set α} {f : α } {K : nnreal} (h : s) {x : α} (hx : x s) {y : α} (hy : y s) :
f x f y + K *
@[protected]
theorem lipschitz_on_with.iff_le_add_mul {α : Type u} {s : set α} {f : α } {K : nnreal} :
s (x : α), x s (y : α), y s f x f y + K *
theorem lipschitz_on_with.bounded_image2 {α : Type u} {β : Type v} {γ : Type w} (f : α β γ) {K₁ K₂ : nnreal} {s : set α} {t : set β} (hs : metric.bounded s) (ht : metric.bounded t) (hf₁ : (b : β), b t (λ (a : α), f a b) s) (hf₂ : (a : α), a s (f a) t) :
theorem continuous_on_prod_of_continuous_on_lipschitz_on {α : Type u} {β : Type v} {γ : Type w} (f : α × β γ) {s : set α} {t : set β} (K : nnreal) (ha : (a : α), a s continuous_on (λ (y : β), f (a, y)) t) (hb : (b : β), b t (λ (x : α), f (x, b)) s) :
(s ×ˢ t)

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical fiber” {a} × t, a ∈ s, and is Lipschitz continuous on each “horizontal fiber” s × {b}, b ∈ t with the same Lipschitz constant K. Then it is continuous on s × t.

The actual statement uses (Lipschitz) continuity of λ y, f (a, y) and λ x, f (x, b) instead of continuity of f on subsets of the product space.

theorem continuous_prod_of_continuous_lipschitz {α : Type u} {β : Type v} {γ : Type w} (f : α × β γ) (K : nnreal) (ha : (a : α), continuous (λ (y : β), f (a, y))) (hb : (b : β), (λ (x : α), f (x, b))) :

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ, a : α, and is Lipschitz continuous on each “horizontal section” univ × {b}, b : β with the same Lipschitz constant K. Then it is continuous.

The actual statement uses (Lipschitz) continuity of λ y, f (a, y) and λ x, f (x, b) instead of continuity of f on subsets of the product space.

theorem continuous_at_of_locally_lipschitz {α : Type u} {β : Type v} {f : α β} {x : α} {r : } (hr : 0 < r) (K : ) (h : (y : α), < r has_dist.dist (f y) (f x) K * ) :

If a function is locally Lipschitz around a point, then it is continuous at this point.

theorem lipschitz_on_with.extend_real {α : Type u} {f : α } {s : set α} {K : nnreal} (hf : s) :
(g : α ), g s

A function f : α → ℝ which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space.

theorem lipschitz_on_with.extend_pi {α : Type u} {ι : Type x} [fintype ι] {f : α ι } {s : set α} {K : nnreal} (hf : s) :
(g : α ι ), g s

A function f : α → (ι → ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz extension to the whole space. TODO: state the same result (with the same proof) for the space ℓ^∞ (ι, ℝ) over a possibly infinite type ι.