# Documentation

Mathlib.Topology.MetricSpace.Lipschitz

# Lipschitz continuous functions #

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 #

• LipschitzWith K f: states that f is Lipschitz with constant K : ℝ≥0
• LipschitzOnWith K f s: states that f is Lipschitz with constant K : ℝ≥0 on a set s
• LipschitzWith.uniformContinuous: a Lipschitz function is uniformly continuous
• LipschitzOnWith.uniformContinuousOn: a function which is Lipschitz on a set s is uniformly continuous on s.

## Implementation notes #

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

def LipschitzWith {α : Type u} {β : Type v} (K : NNReal) (f : αβ) :

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.

Instances For
theorem lipschitzWith_iff_dist_le_mul {α : Type u} {β : Type v} {K : NNReal} {f : αβ} :
∀ (x y : α), dist (f x) (f y) K * dist x y
theorem LipschitzWith.dist_le_mul {α : Type u} {β : Type v} {K : NNReal} {f : αβ} :
∀ (x y : α), dist (f x) (f y) K * dist x y

Alias of the forward direction of lipschitzWith_iff_dist_le_mul.

theorem LipschitzWith.of_dist_le_mul {α : Type u} {β : Type v} {K : NNReal} {f : αβ} :
(∀ (x y : α), dist (f x) (f y) K * dist x y) →

Alias of the reverse direction of lipschitzWith_iff_dist_le_mul.

def LipschitzOnWith {α : Type u} {β : Type v} (K : NNReal) (f : αβ) (s : Set α) :

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.

Instances For
@[simp]
theorem lipschitzOnWith_empty {α : Type u} {β : Type v} (K : NNReal) (f : αβ) :

Every function is Lipschitz on the empty set (with any Lipschitz constant).

theorem LipschitzOnWith.mono {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {t : Set α} {f : αβ} (hf : ) (h : s t) :

Being Lipschitz on a set is monotone w.r.t. that set.

theorem lipschitzOnWith_iff_dist_le_mul {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} :
∀ (x : α), x s∀ (y : α), y sdist (f x) (f y) K * dist x y
theorem LipschitzOnWith.dist_le_mul {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} :
∀ (x : α), x s∀ (y : α), y sdist (f x) (f y) K * dist x y

Alias of the forward direction of lipschitzOnWith_iff_dist_le_mul.

theorem LipschitzOnWith.of_dist_le_mul {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} :
(∀ (x : α), x s∀ (y : α), y sdist (f x) (f y) K * dist x y) →

Alias of the reverse direction of lipschitzOnWith_iff_dist_le_mul.

@[simp]
theorem lipschitzOn_univ {α : Type u} {β : Type v} {K : NNReal} {f : αβ} :
LipschitzOnWith K f Set.univ

f is Lipschitz iff it is Lipschitz on the entire space.

theorem lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {s : Set α} :
theorem LipschitzOnWith.to_restrict {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {s : Set α} :
LipschitzWith K ()

Alias of the forward direction of lipschitzOnWith_iff_restrict.

theorem MapsTo.lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) :
theorem LipschitzOnWith.to_restrict_mapsTo {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {s : Set α} {t : Set β} (h : Set.MapsTo f s t) :
LipschitzWith K ()

Alias of the forward direction of MapsTo.lipschitzOnWith_iff_restrict.

theorem LipschitzWith.lipschitzOnWith {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (h : ) (s : Set α) :
theorem LipschitzWith.edist_le_mul {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (h : ) (x : α) (y : α) :
edist (f x) (f y) K * edist x y
theorem LipschitzWith.edist_le_mul_of_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {x : α} {y : α} {r : ENNReal} (h : ) (hr : edist x y r) :
edist (f x) (f y) K * r
theorem LipschitzWith.edist_lt_mul_of_lt {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {x : α} {y : α} {r : ENNReal} (h : ) (hK : K 0) (hr : edist x y < r) :
edist (f x) (f y) < K * r
theorem LipschitzWith.mapsTo_emetric_closedBall {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (h : ) (x : α) (r : ENNReal) :
Set.MapsTo f () (EMetric.closedBall (f x) (K * r))
theorem LipschitzWith.mapsTo_emetric_ball {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (h : ) (hK : K 0) (x : α) (r : ENNReal) :
Set.MapsTo f () (EMetric.ball (f x) (K * r))
theorem LipschitzWith.edist_lt_top {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) {x : α} {y : α} (h : edist x y ) :
edist (f x) (f y) <
theorem LipschitzWith.mul_edist_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (h : ) (x : α) (y : α) :
(K)⁻¹ * edist (f x) (f y) edist x y
theorem LipschitzWith.of_edist_le {α : Type u} {β : Type v} {f : αβ} (h : ∀ (x y : α), edist (f x) (f y) edist x y) :
theorem LipschitzWith.weaken {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) {K' : NNReal} (h : K K') :
theorem LipschitzWith.ediam_image_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) (s : Set α) :
EMetric.diam (f '' s) K *
theorem LipschitzWith.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) {x : α} {y : α} {d : ENNReal} (h : edist x y < d / K) :
edist (f x) (f y) < d
theorem LipschitzWith.uniformContinuous {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) :

A Lipschitz function is uniformly continuous.

theorem LipschitzWith.continuous {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) :

A Lipschitz function is continuous.

theorem LipschitzWith.const {α : Type u} {β : Type v} (b : β) :
LipschitzWith 0 fun x => b

Constant functions are Lipschitz (with any constant).

theorem LipschitzWith.const' {α : Type u} {β : Type v} (b : β) {K : NNReal} :
LipschitzWith K fun x => b
theorem LipschitzWith.id {α : Type u} :

The identity is 1-Lipschitz.

theorem LipschitzWith.subtype_val {α : Type u} (s : Set α) :
LipschitzWith 1 Subtype.val

The inclusion of a subset is 1-Lipschitz.

theorem LipschitzWith.subtype_mk {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) {p : βProp} (hp : (x : α) → p (f x)) :
LipschitzWith K fun x => { val := f x, property := hp x }
theorem LipschitzWith.eval {ι : Type x} {α : ιType u} [(i : ι) → PseudoEMetricSpace (α i)] [] (i : ι) :
theorem LipschitzWith.restrict {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) (s : Set α) :

The restriction of a K-Lipschitz function is K-Lipschitz.

theorem LipschitzWith.comp {α : Type u} {β : Type v} {γ : Type w} {Kf : NNReal} {Kg : NNReal} {f : βγ} {g : αβ} (hf : ) (hg : ) :
LipschitzWith (Kf * Kg) (f g)

The composition of Lipschitz functions is Lipschitz.

theorem LipschitzWith.comp_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} {Kf : NNReal} {Kg : NNReal} {f : βγ} {g : αβ} {s : Set α} (hf : ) (hg : LipschitzOnWith Kg g s) :
LipschitzOnWith (Kf * Kg) (f g) s
theorem LipschitzWith.prod_fst {α : Type u} {β : Type v} :
LipschitzWith 1 Prod.fst
theorem LipschitzWith.prod_snd {α : Type u} {β : Type v} :
LipschitzWith 1 Prod.snd
theorem LipschitzWith.prod {α : Type u} {β : Type v} {γ : Type w} {f : αβ} {Kf : NNReal} (hf : ) {g : αγ} {Kg : NNReal} (hg : ) :
LipschitzWith (max Kf Kg) fun x => (f x, g x)

If f and g are Lipschitz functions, so is the induced map f × g to the product type.

theorem LipschitzWith.prod_mk_left {α : Type u} {β : Type v} (a : α) :
theorem LipschitzWith.prod_mk_right {α : Type u} {β : Type v} (b : β) :
LipschitzWith 1 fun a => (a, b)
theorem LipschitzWith.uncurry {α : Type u} {β : Type v} {γ : Type w} {f : αβγ} {Kα : NNReal} {Kβ : NNReal} (hα : ∀ (b : β), LipschitzWith fun a => f a b) (hβ : ∀ (a : α), LipschitzWith (f a)) :
LipschitzWith ( + ) ()
theorem LipschitzWith.iterate {α : Type u} {K : NNReal} {f : αα} (hf : ) (n : ) :

Iterates of a Lipschitz function are Lipschitz.

theorem LipschitzWith.edist_iterate_succ_le_geometric {α : Type u} {K : NNReal} {f : αα} (hf : ) (x : α) (n : ) :
edist (f^[n] x) (f^[n + 1] x) edist x (f x) * K ^ n
theorem LipschitzWith.mul {α : Type u} {f : } {g : } {Kf : NNReal} {Kg : NNReal} (hf : ) (hg : ) :
LipschitzWith (Kf * Kg) (f * g)
theorem LipschitzWith.list_prod {α : Type u} {ι : Type x} (f : ι) (K : ιNNReal) (h : ∀ (i : ι), LipschitzWith (K i) (f i)) (l : List ι) :

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

theorem LipschitzWith.pow {α : Type u} {f : } {K : NNReal} (h : ) (n : ) :
LipschitzWith (K ^ n) (f ^ n)
theorem LipschitzWith.of_dist_le' {α : Type u} {β : Type v} {f : αβ} {K : } (h : ∀ (x y : α), dist (f x) (f y) K * dist x y) :
theorem LipschitzWith.mk_one {α : Type u} {β : Type v} {f : αβ} (h : ∀ (x y : α), dist (f x) (f y) dist x y) :
theorem LipschitzWith.of_le_add_mul' {α : Type u} {f : α} (K : ) (h : ∀ (x y : α), f x f y + K * dist x y) :

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

theorem LipschitzWith.of_le_add_mul {α : Type u} {f : α} (K : NNReal) (h : ∀ (x y : α), f x f y + K * dist x y) :

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

theorem LipschitzWith.of_le_add {α : Type u} {f : α} (h : ∀ (x y : α), f x f y + dist x y) :
theorem LipschitzWith.le_add_mul {α : Type u} {f : α} {K : NNReal} (h : ) (x : α) (y : α) :
f x f y + K * dist x y
theorem LipschitzWith.iff_le_add_mul {α : Type u} {f : α} {K : NNReal} :
∀ (x y : α), f x f y + K * dist x y
theorem LipschitzWith.nndist_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) (x : α) (y : α) :
nndist (f x) (f y) K * nndist x y
theorem LipschitzWith.dist_le_mul_of_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {x : α} {y : α} {r : } (hf : ) (hr : dist x y r) :
dist (f x) (f y) K * r
theorem LipschitzWith.mapsTo_closedBall {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) (x : α) (r : ) :
Set.MapsTo f () (Metric.closedBall (f x) (K * r))
theorem LipschitzWith.dist_lt_mul_of_lt {α : Type u} {β : Type v} {K : NNReal} {f : αβ} {x : α} {y : α} {r : } (hf : ) (hK : K 0) (hr : dist x y < r) :
dist (f x) (f y) < K * r
theorem LipschitzWith.mapsTo_ball {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) (hK : K 0) (x : α) (r : ) :
Set.MapsTo f () (Metric.ball (f x) (K * r))
def LipschitzWith.toLocallyBoundedMap {α : Type u} {β : Type v} {K : NNReal} (f : αβ) (hf : ) :

A Lipschitz continuous map is a locally bounded map.

Instances For
@[simp]
theorem LipschitzWith.coe_toLocallyBoundedMap {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) :
= f
theorem LipschitzWith.comap_cobounded_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) :
theorem LipschitzWith.isBounded_image {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) {s : Set α} (hs : ) :

The image of a bounded set under a Lipschitz map is bounded.

theorem LipschitzWith.diam_image_le {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) (s : Set α) (hs : ) :
Metric.diam (f '' s) K *
theorem LipschitzWith.dist_left {α : Type u} (y : α) :
LipschitzWith 1 fun x => dist x y
theorem LipschitzWith.dist_right {α : Type u} (x : α) :
theorem LipschitzWith.dist_iterate_succ_le_geometric {α : Type u} {K : NNReal} {f : αα} (hf : ) (x : α) (n : ) :
dist (f^[n] x) (f^[n + 1] x) dist x (f x) * K ^ n
theorem lipschitzWith_max :
LipschitzWith 1 fun p => max p.fst p.snd
theorem lipschitzWith_min :
LipschitzWith 1 fun p => min p.fst p.snd
theorem LipschitzWith.max {α : Type u} {f : α} {g : α} {Kf : NNReal} {Kg : NNReal} (hf : ) (hg : ) :
LipschitzWith (max Kf Kg) fun x => max (f x) (g x)
theorem LipschitzWith.min {α : Type u} {f : α} {g : α} {Kf : NNReal} {Kg : NNReal} (hf : ) (hg : ) :
LipschitzWith (max Kf Kg) fun x => min (f x) (g x)
theorem LipschitzWith.max_const {α : Type u} {f : α} {Kf : NNReal} (hf : ) (a : ) :
LipschitzWith Kf fun x => max (f x) a
theorem LipschitzWith.const_max {α : Type u} {f : α} {Kf : NNReal} (hf : ) (a : ) :
LipschitzWith Kf fun x => max a (f x)
theorem LipschitzWith.min_const {α : Type u} {f : α} {Kf : NNReal} (hf : ) (a : ) :
LipschitzWith Kf fun x => min (f x) a
theorem LipschitzWith.const_min {α : Type u} {f : α} {Kf : NNReal} (hf : ) (a : ) :
LipschitzWith Kf fun x => min a (f x)
theorem LipschitzWith.projIcc {a : } {b : } (h : a b) :
theorem LipschitzOnWith.uniformContinuousOn {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} (hf : ) :
theorem LipschitzOnWith.continuousOn {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} (hf : ) :
theorem LipschitzOnWith.edist_le_mul_of_le {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} {x : α} {y : α} {r : ENNReal} (h : ) (hx : x s) (hy : y s) (hr : edist x y r) :
edist (f x) (f y) K * r
theorem LipschitzOnWith.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} (hf : ) {x : α} {y : α} (hx : x s) (hy : y s) {d : ENNReal} (hd : edist x y < d / K) :
edist (f x) (f y) < d
theorem LipschitzOnWith.comp {α : Type u} {β : Type v} {γ : Type w} {K : NNReal} {s : Set α} {f : αβ} {g : βγ} {t : Set β} {Kg : NNReal} (hg : LipschitzOnWith Kg g t) (hf : ) (hmaps : Set.MapsTo f s t) :
LipschitzOnWith (Kg * K) (g f) s
theorem LipschitzOnWith.of_dist_le' {α : Type u} {β : Type v} {s : Set α} {f : αβ} {K : } (h : ∀ (x : α), x s∀ (y : α), y sdist (f x) (f y) K * dist x y) :
theorem LipschitzOnWith.mk_one {α : Type u} {β : Type v} {s : Set α} {f : αβ} (h : ∀ (x : α), x s∀ (y : α), y sdist (f x) (f y) dist x y) :
theorem LipschitzOnWith.of_le_add_mul' {α : Type u} {s : Set α} {f : α} (K : ) (h : ∀ (x : α), x s∀ (y : α), y sf x f y + K * dist x y) :

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

theorem LipschitzOnWith.of_le_add_mul {α : Type u} {s : Set α} {f : α} (K : NNReal) (h : ∀ (x : α), x s∀ (y : α), y sf x f y + K * dist x y) :

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

theorem LipschitzOnWith.of_le_add {α : Type u} {s : Set α} {f : α} (h : ∀ (x : α), x s∀ (y : α), y sf x f y + dist x y) :
theorem LipschitzOnWith.le_add_mul {α : Type u} {s : Set α} {f : α} {K : NNReal} (h : ) {x : α} (hx : x s) {y : α} (hy : y s) :
f x f y + K * dist x y
theorem LipschitzOnWith.iff_le_add_mul {α : Type u} {s : Set α} {f : α} {K : NNReal} :
∀ (x : α), x s∀ (y : α), y sf x f y + K * dist x y
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [] (f : α × βγ) {s : Set α} {s' : Set α} {t : Set β} (hs' : s' s) (hss' : s closure s') (K : NNReal) (ha : ∀ (a : α), a s'ContinuousOn (fun y => f (a, y)) t) (hb : ∀ (b : β), b tLipschitzOnWith K (fun x => f (x, b)) s) :

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. Moreover, it suffices to require continuity on vertical fibers for a from a subset s' ⊆ s that is dense in s.

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

theorem continuousOn_prod_of_continuousOn_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [] (f : α × βγ) {s : Set α} {t : Set β} (K : NNReal) (ha : ∀ (a : α), a sContinuousOn (fun y => f (a, y)) t) (hb : ∀ (b : β), b tLipschitzOnWith K (fun x => f (x, b)) s) :

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 fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

theorem continuous_prod_of_dense_continuous_lipschitzWith {α : Type u} {β : Type v} {γ : Type w} [] (f : α × βγ) (K : NNReal) {s : Set α} (hs : ) (ha : ∀ (a : α), a sContinuous fun y => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)) :

Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ for a : α from a dense set. Suppose that it 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 fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

theorem continuous_prod_of_continuous_lipschitzWith {α : Type u} {β : Type v} {γ : Type w} [] (f : α × βγ) (K : NNReal) (ha : ∀ (a : α), Continuous fun y => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun 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 fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

theorem continuousAt_of_locally_lipschitz {α : Type u} {β : Type v} {f : αβ} {x : α} {r : } (hr : 0 < r) (K : ) (h : ∀ (y : α), dist y x < rdist (f y) (f x) K * dist y x) :

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

theorem LipschitzOnWith.extend_real {α : Type u} {f : α} {s : Set α} {K : NNReal} (hf : ) :
g, Set.EqOn f g s

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

theorem LipschitzOnWith.extend_pi {α : Type u} {ι : Type x} [] {f : αι} {s : Set α} {K : NNReal} (hf : ) :
g, Set.EqOn f g s

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