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} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} : LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y

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

Alias of the reverse direction of lipschitzWith_iff_dist_le_mul.

theorem LipschitzWith.dist_le_mul {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} : LipschitzWith K f → ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y

Alias of the forward direction of lipschitzWith_iff_dist_le_mul.

theorem lipschitzOnWith_iff_dist_le_mul {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y

theorem LipschitzOnWith.dist_le_mul {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : LipschitzOnWith K f s → ∀ x ∈ s, ∀ y ∈ s, dist (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} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} : (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y) → LipschitzOnWith K f s

Alias of the reverse direction of lipschitzOnWith_iff_dist_le_mul.

theorem LipschitzWith.of_dist_le' {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {K : ℝ} (h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y) : LipschitzWith (Real.toNNReal K) f

theorem LipschitzWith.mk_one {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} (h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y) : LipschitzWith 1 f

theorem LipschitzWith.of_le_add_mul' {α : Type u} [PseudoMetricSpace α] {f : α → ℝ} (K : ℝ) (h : ∀ (x y : α), f x ≤ f y + K * dist x y) : LipschitzWith (Real.toNNReal 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 LipschitzWith.of_le_add_mul {α : Type u} [PseudoMetricSpace α] {f : α → ℝ} (K : NNReal) (h : ∀ (x y : α), f x ≤ f y + ↑K * dist x y) : LipschitzWith K f

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} [PseudoMetricSpace α] {f : α → ℝ} (h : ∀ (x y : α), f x ≤ f y + dist x y) : LipschitzWith 1 f

theorem LipschitzWith.le_add_mul {α : Type u} [PseudoMetricSpace α] {f : α → ℝ} {K : NNReal} (h : LipschitzWith K f) (x : α) (y : α) : f x ≤ f y + ↑K * dist x y

theorem LipschitzWith.iff_le_add_mul {α : Type u} [PseudoMetricSpace α] {f : α → ℝ} {K : NNReal} : LipschitzWith K f ↔ ∀ (x y : α), f x ≤ f y + ↑K * dist x y

theorem LipschitzWith.nndist_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (x : α) (y : α) : nndist (f x) (f y) ≤ K * nndist x y

theorem LipschitzWith.dist_le_mul_of_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} {x : α} {y : α} {r : ℝ} (hf : LipschitzWith K f) (hr : dist x y ≤ r) : dist (f x) (f y) ≤ ↑K * r

theorem LipschitzWith.mapsTo_closedBall {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (x : α) (r : ℝ) : Set.MapsTo f (Metric.closedBall x r) (Metric.closedBall (f x) (↑K * r))

theorem LipschitzWith.dist_lt_mul_of_lt {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} {x : α} {y : α} {r : ℝ} (hf : LipschitzWith K f) (hK : K ≠ 0) (hr : dist x y < r) : dist (f x) (f y) < ↑K * r

theorem LipschitzWith.mapsTo_ball {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (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} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} (f : α → β) (hf : LipschitzWith K f) : LocallyBoundedMap α β

A Lipschitz continuous map is a locally bounded map.

Equations

• LipschitzWith.toLocallyBoundedMap f hf = LocallyBoundedMap.ofMapBounded f ⋯

@[simp]

theorem LipschitzWith.coe_toLocallyBoundedMap {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) : ⇑(LipschitzWith.toLocallyBoundedMap f hf) = f

theorem LipschitzWith.comap_cobounded_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) : Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α

theorem LipschitzWith.isBounded_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {s : Set α} (hs : Bornology.IsBounded s) : Bornology.IsBounded (f '' s)

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

theorem LipschitzWith.diam_image_le {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) (hs : Bornology.IsBounded s) : Metric.diam (f '' s) ≤ ↑K * Metric.diam s

theorem LipschitzWith.dist_left {α : Type u} [PseudoMetricSpace α] (y : α) : LipschitzWith 1 fun (x : α) => dist x y

theorem LipschitzWith.dist_right {α : Type u} [PseudoMetricSpace α] (x : α) : LipschitzWith 1 (dist x)

theorem LipschitzWith.dist {α : Type u} [PseudoMetricSpace α] : LipschitzWith 2 (Function.uncurry dist)

theorem LipschitzWith.dist_iterate_succ_le_geometric {α : Type u} [PseudoMetricSpace α] {K : NNReal} {f : α → α} (hf : LipschitzWith K f) (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 Real.lipschitzWith_toNNReal : LipschitzWith 1 Real.toNNReal

theorem LipschitzWith.cauchySeq_comp {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {u : ℕ → α} (hu : CauchySeq u) : CauchySeq (f ∘ u)

theorem LipschitzWith.max {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {g : α → ℝ} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun (x : α) => max (f x) (g x)

theorem LipschitzWith.min {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {g : α → ℝ} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun (x : α) => min (f x) (g x)

theorem LipschitzWith.max_const {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal} (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun (x : α) => max (f x) a

theorem LipschitzWith.const_max {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal} (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun (x : α) => max a (f x)

theorem LipschitzWith.min_const {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal} (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun (x : α) => min (f x) a

theorem LipschitzWith.const_min {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {Kf : NNReal} (hf : LipschitzWith Kf f) (a : ℝ) : LipschitzWith Kf fun (x : α) => min a (f x)

theorem LipschitzWith.projIcc {a : ℝ} {b : ℝ} (h : a ≤ b) : LipschitzWith 1 (Set.projIcc a b h)

theorem LipschitzOnWith.of_dist_le' {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {f : α → β} {K : ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ K * dist x y) : LipschitzOnWith (Real.toNNReal K) f s

theorem LipschitzOnWith.mk_one {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {f : α → β} (h : ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) : LipschitzOnWith 1 f s

theorem LipschitzOnWith.of_le_add_mul' {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : ℝ) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) : LipschitzOnWith (Real.toNNReal K) 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} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : NNReal) (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y) : LipschitzOnWith K f s

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} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (h : ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + dist x y) : LipschitzOnWith 1 f s

theorem LipschitzOnWith.le_add_mul {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} {K : NNReal} (h : LipschitzOnWith K f s) {x : α} (hx : x ∈ s) {y : α} (hy : y ∈ s) : f x ≤ f y + ↑K * dist x y

theorem LipschitzOnWith.iff_le_add_mul {α : Type u} [PseudoMetricSpace α] {s : Set α} {f : α → ℝ} {K : NNReal} : LipschitzOnWith K f s ↔ ∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y

theorem LipschitzOnWith.isBounded_image2 {α : Type u} {β : Type v} {γ : Type w} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] (f : α → β → γ) {K₁ : NNReal} {K₂ : NNReal} {s : Set α} {t : Set β} (hs : Bornology.IsBounded s) (ht : Bornology.IsBounded t) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (fun (a : α) => f a b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) : Bornology.IsBounded (Set.image2 f s t)

theorem LipschitzOnWith.cauchySeq_comp {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) {u : ℕ → α} (hu : CauchySeq u) (h'u : Set.range u ⊆ s) : CauchySeq (f ∘ u)

theorem LocallyLipschitz.min {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} {g : α → ℝ} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz fun (x : α) => min (f x) (g x)

The minimum of locally Lipschitz functions is locally Lipschitz.

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

The maximum of locally Lipschitz functions is locally Lipschitz.

theorem LocallyLipschitz.max_const {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun (x : α) => max (f x) a

theorem LocallyLipschitz.const_max {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun (x : α) => max a (f x)

theorem LocallyLipschitz.min_const {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun (x : α) => min (f x) a

theorem LocallyLipschitz.const_min {α : Type u} [PseudoEMetricSpace α] {f : α → ℝ} (hf : LocallyLipschitz f) (a : ℝ) : LocallyLipschitz fun (x : α) => min a (f x)

theorem continuousAt_of_locally_lipschitz {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : α → β} {x : α} {r : ℝ} (hr : 0 < r) (K : ℝ) (h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x) : ContinuousAt f x

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

theorem LipschitzOnWith.extend_real {α : Type u} [PseudoMetricSpace α] {f : α → ℝ} {s : Set α} {K : NNReal} (hf : LipschitzOnWith K f s) : ∃ (g : α → ℝ), LipschitzWith K 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} [PseudoMetricSpace α] [Fintype ι] {f : α → ι → ℝ} {s : Set α} {K : NNReal} (hf : LipschitzOnWith K f s) : ∃ (g : α → ι → ℝ), LipschitzWith K 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.