mathlib documentation

topology.metric_space.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

Implementation notes

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

def lipschitz_with {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] :
ℝ≥0(α → β) → 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} [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β} :
lipschitz_with K f ∀ (x y : α), dist (f x) (f y) (K) * dist x y

def lipschitz_on_with {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] :
ℝ≥0(α → β)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} [emetric_space α] [emetric_space β] (K : ℝ≥0) (f : α → β) :

theorem lipschitz_on_with.mono {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {s t : set α} {f : α → β} :
lipschitz_on_with K f ts tlipschitz_on_with K f s

theorem lipschitz_on_with_iff_dist_le_mul {α : Type u} {β : Type v} [metric_space α] [metric_space β] {K : ℝ≥0} {s : set α} {f : α → β} :
lipschitz_on_with K f s ∀ (x : α), x s∀ (y : α), y sdist (f x) (f y) (K) * dist x y

@[simp]
theorem lipschitz_on_univ {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} :

theorem lipschitz_on_with_iff_restrict {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} {s : set α} :

theorem lipschitz_with.edist_le_mul {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (h : lipschitz_with K f) (x y : α) :
edist (f x) (f y) (K) * edist x y

theorem lipschitz_with.edist_lt_top {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) {x y : α} :
edist x y < edist (f x) (f y) <

theorem lipschitz_with.mul_edist_le {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (h : lipschitz_with K f) (x y : α) :
(K)⁻¹ * edist (f x) (f y) edist x y

theorem lipschitz_with.of_edist_le {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {f : α → β} :
(∀ (x y : α), edist (f x) (f y) edist x y)lipschitz_with 1 f

theorem lipschitz_with.weaken {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) {K' : ℝ≥0} :
K K'lipschitz_with K' f

theorem lipschitz_with.ediam_image_le {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) (s : set α) :

theorem lipschitz_with.uniform_continuous {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} :

A Lipschitz function is uniformly continuous

theorem lipschitz_with.continuous {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} :

A Lipschitz function is continuous

theorem lipschitz_with.const {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] (b : β) :
lipschitz_with 0 (λ (a : α), b)

theorem lipschitz_with.id {α : Type u} [emetric_space α] :

theorem lipschitz_with.subtype_coe {α : Type u} [emetric_space α] (s : set α) :

theorem lipschitz_with.restrict {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) (s : set α) :

theorem lipschitz_with.comp {α : Type u} {β : Type v} {γ : Type w} [emetric_space α] [emetric_space β] [emetric_space γ] {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} :
lipschitz_with Kf flipschitz_with Kg glipschitz_with (Kf * Kg) (f g)

theorem lipschitz_with.prod_fst {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] :

theorem lipschitz_with.prod_snd {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] :

theorem lipschitz_with.prod {α : Type u} {β : Type v} {γ : Type w} [emetric_space α] [emetric_space β] [emetric_space γ] {f : α → β} {Kf : ℝ≥0} (hf : lipschitz_with Kf f) {g : α → γ} {Kg : ℝ≥0} :
lipschitz_with Kg glipschitz_with (max Kf Kg) (λ (x : α), (f x, g x))

theorem lipschitz_with.uncurry {α : Type u} {β : Type v} {γ : Type w} [emetric_space α] [emetric_space β] [emetric_space γ] {f : α → β → γ} {Kα Kβ : ℝ≥0} :
(∀ (b : β), lipschitz_with (λ (a : α), f a b))(∀ (a : α), lipschitz_with (f a))lipschitz_with (Kα + Kβ) (function.uncurry f)

theorem lipschitz_with.iterate {α : Type u} [emetric_space α] {K : ℝ≥0} {f : α → α} (hf : lipschitz_with K f) (n : ) :

theorem lipschitz_with.edist_iterate_succ_le_geometric {α : Type u} [emetric_space α] {K : ℝ≥0} {f : α → α} (hf : lipschitz_with K f) (x : α) (n : ) :
edist (f^[n] x) (f^[n + 1] x) (edist x (f x)) * K ^ n

theorem lipschitz_with.mul {α : Type u} [emetric_space α] {f g : category_theory.End α} {Kf Kg : ℝ≥0} :
lipschitz_with Kf flipschitz_with Kg glipschitz_with (Kf * Kg) (f * g)

theorem lipschitz_with.list_prod {α : Type u} {ι : Type x} [emetric_space α] (f : ι → category_theory.End α) (K : ι → ℝ≥0) (h : ∀ (i : ι), lipschitz_with (K i) (f i)) (l : list ι) :

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

theorem lipschitz_with.pow {α : Type u} [emetric_space α] {f : category_theory.End α} {K : ℝ≥0} (h : lipschitz_with K f) (n : ) :
lipschitz_with (K ^ n) (f ^ n)

theorem lipschitz_with.of_dist_le' {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {K : } :
(∀ (x y : α), dist (f x) (f y) K * dist x y)lipschitz_with (nnreal.of_real K) f

theorem lipschitz_with.mk_one {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} :
(∀ (x y : α), dist (f x) (f y) dist x y)lipschitz_with 1 f

theorem lipschitz_with.of_le_add_mul' {α : Type u} [metric_space α] {f : α → } (K : ) :
(∀ (x y : α), f x f y + K * dist x y)lipschitz_with (nnreal.of_real K) f

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

theorem lipschitz_with.of_le_add_mul {α : Type u} [metric_space α] {f : α → } (K : ℝ≥0) :
(∀ (x y : α), f x f y + (K) * dist x y)lipschitz_with K f

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

theorem lipschitz_with.of_le_add {α : Type u} [metric_space α] {f : α → } :
(∀ (x y : α), f x f y + dist x y)lipschitz_with 1 f

theorem lipschitz_with.le_add_mul {α : Type u} [metric_space α] {f : α → } {K : ℝ≥0} (h : lipschitz_with K f) (x y : α) :
f x f y + (K) * dist x y

theorem lipschitz_with.iff_le_add_mul {α : Type u} [metric_space α] {f : α → } {K : ℝ≥0} :
lipschitz_with K f ∀ (x y : α), f x f y + (K) * dist x y

theorem lipschitz_with.nndist_le {α : Type u} {β : Type v} [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) (x y : α) :
nndist (f x) (f y) K * nndist x y

theorem lipschitz_with.diam_image_le {α : Type u} {β : Type v} [metric_space α] [metric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K f) (s : set α) :

theorem lipschitz_with.dist_left {α : Type u} [metric_space α] (y : α) :
lipschitz_with 1 (λ (x : α), dist x y)

theorem lipschitz_with.dist_right {α : Type u} [metric_space α] (x : α) :

theorem lipschitz_with.dist_iterate_succ_le_geometric {α : Type u} [metric_space α] {K : ℝ≥0} {f : α → α} (hf : lipschitz_with K f) (x : α) (n : ) :
dist (f^[n] x) (f^[n + 1] x) (dist x (f x)) * K ^ n

theorem lipschitz_on_with.uniform_continuous_on {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {s : set α} {f : α → β} :

theorem lipschitz_on_with.continuous_on {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {s : set α} {f : α → β} :

theorem continuous_at_of_locally_lipschitz {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {x : α} {r : } (hr : 0 < r) (K : ) :
(∀ (y : α), dist y x < rdist (f y) (f x) K * dist y x)continuous_at f x

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