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

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 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 β] (K : ℝ≥0) (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

lipschitz_with K f = ∀ (x y : α), edist (f x) (f y) ≤ (↑K) * edist x y

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 β] (K : ℝ≥0) (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

lipschitz_on_with K f s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → edist (f x) (f y) ≤ (↑K) * edist x y

@[simp]

theorem lipschitz_on_with_empty {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] (K : ℝ≥0) (f : α → β) :

lipschitz_on_with K f ∅

theorem lipschitz_on_with.mono {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {s t : set α} {f : α → β} (hf : lipschitz_on_with K f t) (h : s ⊆ t) :

lipschitz_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 ∈ s → dist (f x) (f y) ≤ (↑K) * dist x y

@[simp]

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

lipschitz_on_with K f set.univ ↔ lipschitz_with K f

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

lipschitz_on_with K f s ↔ lipschitz_with K (set.restrict f s)

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 : α} (h : 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 : α → β} (h : ∀ (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} (h : 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 α) :

emetric.diam (f '' s) ≤ (↑K) * emetric.diam s

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

uniform_continuous f

A Lipschitz function is uniformly continuous

theorem lipschitz_with.continuous {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {K : ℝ≥0} {f : α → β} (hf : lipschitz_with K 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 α] :

lipschitz_with 1 id

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

lipschitz_with 1 subtype.val

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

lipschitz_with 1 coe

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

lipschitz_with K (set.restrict f s)

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

lipschitz_with (Kf * Kg) (f ∘ g)

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

lipschitz_with 1 prod.fst

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

lipschitz_with 1 prod.snd

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} (hg : lipschitz_with Kg g) :

lipschitz_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} (hα : ∀ (b : β), lipschitz_with Kα (λ (a : α), f a b)) (hβ : ∀ (a : α), lipschitz_with Kβ (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 : ℕ) :

lipschitz_with (K ^ n) 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} (hf : lipschitz_with Kf f) (hg : lipschitz_with Kg g) :

lipschitz_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 ι) :

lipschitz_with (list.map K l).prod (list.map f l).prod

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 : ℝ} (h : ∀ (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 : α → β} (h : ∀ (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 : ℝ) (h : ∀ (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) (h : ∀ (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 : α → ℝ} (h : ∀ (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 α) (hs : metric.bounded s) :

metric.diam (f '' s) ≤ (↑K) * metric.diam s

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 : α) :

lipschitz_with 1 (dist x)

theorem lipschitz_with.dist {α : Type u} [metric_space α] :

lipschitz_with 2 (function.uncurry dist)

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 : α → β} (hf : lipschitz_on_with K f s) :

uniform_continuous_on f s

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

continuous_on f s

theorem continuous_at_of_locally_lipschitz {α : Type u} {β : Type v} [metric_space α] [metric_space β] {f : α → β} {x : α} {r : ℝ} (hr : 0 < r) (K : ℝ) (h : ∀ (y : α), dist y x < r → dist (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.