Documentation

Mathlib.Topology.MetricSpace.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. 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.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 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 lipschitzOnWith_iff_dist_le_mul {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} :
LipschitzOnWith K f s xs, ys, dist (f x) (f y) K * dist x y
theorem LipschitzOnWith.of_dist_le_mul {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} :
(∀ xs, ys, 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 LipschitzOnWith.dist_le_mul {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} :
LipschitzOnWith K f sxs, 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} [PseudoMetricSpace α] [PseudoMetricSpace β] {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} [PseudoMetricSpace α] [PseudoMetricSpace β] {f : αβ} (h : ∀ (x y : α), dist (f x) (f y) dist x y) :
theorem LipschitzWith.of_le_add_mul' {α : Type u} [PseudoMetricSpace α] {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} [PseudoMetricSpace α] {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} [PseudoMetricSpace α] {f : α} (h : ∀ (x y : α), f x f y + dist x y) :
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 : ) :
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) :

A Lipschitz continuous map is a locally bounded map.

Equations
Instances For
    @[simp]
    theorem LipschitzWith.coe_toLocallyBoundedMap {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) :
    theorem LipschitzWith.isBounded_image {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) {s : Set α} (hs : Bornology.IsBounded 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) :
    theorem LipschitzWith.dist_left {α : Type u} [PseudoMetricSpace α] (y : α) :
    LipschitzWith 1 fun (x : α) => dist x y
    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 LipschitzWith.cauchySeq_comp {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) {u : α} (hu : CauchySeq 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) :
    theorem LipschitzOnWith.of_dist_le' {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {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} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {f : αβ} (h : xs, ys, dist (f x) (f y) dist x y) :
    theorem LipschitzOnWith.of_le_add_mul' {α : Type u} [PseudoMetricSpace α] {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} [PseudoMetricSpace α] {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} [PseudoMetricSpace α] {s : Set α} {f : α} (h : xs, ys, f x f y + dist x y) :
    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 xs, ys, 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₁ : bt, LipschitzOnWith K₁ (fun (a : α) => f a b) s) (hf₂ : as, LipschitzOnWith K₂ (f a) 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) :
    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 < 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} [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.