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. Finally, f : α → β is called locally Lipschitz continuous if each x : α has a neighbourhood on which f is Lipschitz continuous (with some constant).

In this file we specialize various facts about Lipschitz continuous maps to the case of (pseudo) metric spaces.

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.

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.

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

Alias of the reverse direction of lipschitzOnWith_iff_dist_le_mul.

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

Alias of the forward direction of lipschitzOnWith_iff_dist_le_mul.

theorem LipschitzWith.of_dist_le' {α : Type u} {β : Type v} {f : αβ} {K : } (h : ∀ (x y : α), dist (f x) (f y) K * dist x y) :
LipschitzWith K.toNNReal f
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) :
LipschitzWith K.toNNReal f

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 x r) (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.

Equations
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.1 p.2
theorem lipschitzWith_min :
LipschitzWith 1 fun (p : ) => min p.1 p.2
theorem LipschitzWith.cauchySeq_comp {α : Type u} {β : Type v} {K : NNReal} {f : αβ} (hf : ) {u : α} (hu : ) :
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.of_dist_le' {α : Type u} {β : Type v} {s : Set α} {f : αβ} {K : } (h : xs, ys, dist (f x) (f y) K * dist x y) :
LipschitzOnWith K.toNNReal f s
theorem LipschitzOnWith.mk_one {α : Type u} {β : Type v} {s : Set α} {f : αβ} (h : xs, ys, dist (f x) (f y) dist x y) :
theorem LipschitzOnWith.of_le_add_mul' {α : Type u} {s : Set α} {f : α} (K : ) (h : xs, ys, f x f y + K * dist x y) :
LipschitzOnWith K.toNNReal f s

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 : xs, ys, 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 LipschitzOnWith.of_le_add {α : Type u} {s : Set α} {f : α} (h : xs, ys, f 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} :
xs, ys, f x f y + K * dist x y
theorem LipschitzOnWith.isBounded_image2 {α : Type u} {β : Type v} {γ : Type w} (f : αβγ) {K₁ : NNReal} {K₂ : NNReal} {s : Set α} {t : Set β} (hs : ) (ht : ) (hf₁ : bt, LipschitzOnWith K₁ (fun (a : α) => f a b) s) (hf₂ : as, LipschitzOnWith K₂ (f a) t) :
theorem LipschitzOnWith.cauchySeq_comp {α : Type u} {β : Type v} {K : NNReal} {s : Set α} {f : αβ} (hf : ) {u : α} (hu : ) (h'u : s) :
theorem LocallyLipschitz.min {α : Type u} {f : α} {g : α} (hf : ) (hg : ) :
LocallyLipschitz fun (x : α) => min (f x) (g x)

The minimum of locally Lipschitz functions is locally Lipschitz.

theorem LocallyLipschitz.max {α : Type u} {f : α} {g : α} (hf : ) (hg : ) :
LocallyLipschitz fun (x : α) => max (f x) (g x)

The maximum of locally Lipschitz functions is locally Lipschitz.

theorem LocallyLipschitz.max_const {α : Type u} {f : α} (hf : ) (a : ) :
LocallyLipschitz fun (x : α) => max (f x) a
theorem LocallyLipschitz.const_max {α : Type u} {f : α} (hf : ) (a : ) :
LocallyLipschitz fun (x : α) => max a (f x)
theorem LocallyLipschitz.min_const {α : Type u} {f : α} (hf : ) (a : ) :
LocallyLipschitz fun (x : α) => min (f x) a
theorem LocallyLipschitz.const_min {α : Type u} {f : α} (hf : ) (a : ) :
LocallyLipschitz fun (x : α) => min a (f x)
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.