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.
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.
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 β] :
nnreal → (α → β) → 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 : α), has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y
theorem
lipschitz_with_iff_dist_le_mul
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{K : nnreal}
{f : α → β} :
lipschitz_with K f ↔ ∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y
theorem
lipschitz_with.edist_le_mul
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(x y : α) :
has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y
theorem
lipschitz_with.edist_lt_top
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{x y : α} :
has_edist.edist x y < ⊤ → has_edist.edist (f x) (f y) < ⊤
theorem
lipschitz_with.mul_edist_le
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(x y : α) :
(↑K)⁻¹ * has_edist.edist (f x) (f y) ≤ has_edist.edist x y
theorem
lipschitz_with.of_edist_le
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{f : α → β} :
(∀ (x y : α), has_edist.edist (f x) (f y) ≤ has_edist.edist x y) → lipschitz_with 1 f
theorem
lipschitz_with.weaken
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{K' : nnreal} :
K ≤ K' → lipschitz_with K' f
theorem
lipschitz_with.ediam_image_le
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{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 : nnreal}
{f : α → β} :
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 : nnreal}
{f : α → β} :
lipschitz_with K f → continuous 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.restrict
{α : Type u}
{β : Type v}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{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 : nnreal}
{f : β → γ}
{g : α → β} :
lipschitz_with Kf f → lipschitz_with Kg g → lipschitz_with (Kf * Kg) (f ∘ g)
theorem
lipschitz_with.prod
{α : Type u}
{β : Type v}
{γ : Type w}
[emetric_space α]
[emetric_space β]
[emetric_space γ]
{f : α → β}
{Kf : nnreal}
(hf : lipschitz_with Kf f)
{g : α → γ}
{Kg : nnreal} :
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β : nnreal} :
(∀ (b : β), lipschitz_with Kα (λ (a : α), f a b)) → (∀ (a : α), lipschitz_with Kβ (f a)) → lipschitz_with (Kα + Kβ) (function.uncurry f)
theorem
lipschitz_with.iterate
{α : Type u}
[emetric_space α]
{K : nnreal}
{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 : nnreal}
{f : α → α}
(hf : lipschitz_with K f)
(x : α)
(n : ℕ) :
theorem
lipschitz_with.mul
{α : Type u}
[emetric_space α]
{f g : category_theory.End α}
{Kf Kg : nnreal} :
lipschitz_with Kf f → 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 : ι → nnreal)
(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 : nnreal}
(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 : α), has_dist.dist (f x) (f y) ≤ K * has_dist.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 : α), has_dist.dist (f x) (f y) ≤ has_dist.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 * has_dist.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 : nnreal) :
(∀ (x y : α), f x ≤ f y + ↑K * has_dist.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 + has_dist.dist x y) → lipschitz_with 1 f
theorem
lipschitz_with.le_add_mul
{α : Type u}
[metric_space α]
{f : α → ℝ}
{K : nnreal}
(h : lipschitz_with K f)
(x y : α) :
f x ≤ f y + ↑K * has_dist.dist x y
theorem
lipschitz_with.iff_le_add_mul
{α : Type u}
[metric_space α]
{f : α → ℝ}
{K : nnreal} :
lipschitz_with K f ↔ ∀ (x y : α), f x ≤ f y + ↑K * has_dist.dist x y
theorem
lipschitz_with.nndist_le
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(x y : α) :
theorem
lipschitz_with.diam_image_le
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(s : set α) :
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 : α), has_dist.dist x y)
theorem
lipschitz_with.dist_right
{α : Type u}
[metric_space α]
(x : α) :
lipschitz_with 1 (has_dist.dist x)
theorem
lipschitz_with.dist_iterate_succ_le_geometric
{α : Type u}
[metric_space α]
{K : nnreal}
{f : α → α}
(hf : lipschitz_with K f)
(x : α)
(n : ℕ) :
theorem
continuous_at_of_locally_lipschitz
{α : Type u}
{β : Type v}
[metric_space α]
[metric_space β]
{f : α → β}
{x : α}
{r : ℝ}
(hr : 0 < r)
(K : ℝ) :
(∀ (y : α), has_dist.dist y x < r → has_dist.dist (f y) (f x) ≤ K * has_dist.dist y x) → continuous_at f x
If a function is locally Lipschitz around a point, then it is continuous at this point.