Documentation

Mathlib.Topology.EMetricSpace.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 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, and that locally Lipschitz functions are continuous.

Main definitions and lemmas #

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.

def LipschitzWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : αβ) :

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
Instances For
    def LipschitzOnWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : αβ) (s : Set α) :

    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
    Instances For
      def LocallyLipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : αβ) :

      f : α → β is called locally Lipschitz continuous iff every point x has a neighbourhood on which f is Lipschitz.

      Equations
      Instances For
        def LocallyLipschitzOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (s : Set α) (f : αβ) :

        f : α → β is called locally Lipschitz continuous on s iff every point x of s has a neighbourhood within s on which f is Lipschitz.

        Equations
        Instances For
          @[simp]
          theorem lipschitzOnWith_empty {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : αβ) :

          Every function is Lipschitz on the empty set (with any Lipschitz constant).

          @[simp]
          theorem locallyLipschitzOn_empty {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : αβ) :
          theorem LipschitzOnWith.mono {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {t : Set α} {f : αβ} (hf : LipschitzOnWith K f t) (h : s t) :

          Being Lipschitz on a set is monotone w.r.t. that set.

          theorem LocallyLipschitzOn.mono {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {t : Set α} {f : αβ} (hf : LocallyLipschitzOn t f) (h : s t) :
          @[simp]
          theorem lipschitzOnWith_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} :

          f is Lipschitz iff it is Lipschitz on the entire space.

          @[deprecated lipschitzOnWith_univ]
          theorem lipschitzOn_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} :

          Alias of lipschitzOnWith_univ.


          f is Lipschitz iff it is Lipschitz on the entire space.

          @[simp]
          theorem locallyLipschitzOn_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} :
          theorem lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} :
          LipschitzOnWith K f s LipschitzWith K (s.restrict f)
          theorem lipschitzOnWith_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} {t : Set s} :
          LipschitzOnWith K (s.restrict f) t LipschitzOnWith K f (s Subtype.val '' t)
          theorem locallyLipschitzOn_iff_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {f : αβ} :
          theorem LipschitzOnWith.to_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} :
          LipschitzOnWith K f sLipschitzWith K (s.restrict f)

          Alias of the forward direction of lipschitzOnWith_iff_restrict.

          theorem LocallyLipschitzOn.restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {s : Set α} {f : αβ} :
          LocallyLipschitzOn s fLocallyLipschitz (s.restrict f)

          Alias of the forward direction of locallyLipschitzOn_iff_restrict.

          theorem Set.MapsTo.lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} {t : Set β} (h : Set.MapsTo f s t) :
          theorem LipschitzOnWith.to_restrict_mapsTo {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} {t : Set β} (h : Set.MapsTo f s t) :

          Alias of the forward direction of Set.MapsTo.lipschitzOnWith_iff_restrict.

          theorem LipschitzWith.lipschitzOnWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} {s : Set α} (h : LipschitzWith K f) :
          theorem LipschitzWith.edist_le_mul {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (h : LipschitzWith K f) (x : α) (y : α) :
          edist (f x) (f y) K * edist x y
          theorem LipschitzWith.edist_le_mul_of_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} {x : α} {y : α} {r : ENNReal} (h : LipschitzWith K f) (hr : edist x y r) :
          edist (f x) (f y) K * r
          theorem LipschitzWith.edist_lt_mul_of_lt {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} {x : α} {y : α} {r : ENNReal} (h : LipschitzWith K f) (hK : K 0) (hr : edist x y < r) :
          edist (f x) (f y) < K * r
          theorem LipschitzWith.mapsTo_emetric_closedBall {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (h : LipschitzWith K f) (x : α) (r : ENNReal) :
          theorem LipschitzWith.mapsTo_emetric_ball {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (h : LipschitzWith K f) (hK : K 0) (x : α) (r : ENNReal) :
          Set.MapsTo f (EMetric.ball x r) (EMetric.ball (f x) (K * r))
          theorem LipschitzWith.edist_lt_top {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) {x : α} {y : α} (h : edist x y ) :
          edist (f x) (f y) <
          theorem LipschitzWith.mul_edist_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (h : LipschitzWith K f) (x : α) (y : α) :
          (↑K)⁻¹ * edist (f x) (f y) edist x y
          theorem LipschitzWith.of_edist_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} (h : ∀ (x y : α), edist (f x) (f y) edist x y) :
          theorem LipschitzWith.weaken {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) {K' : NNReal} (h : K K') :
          theorem LipschitzWith.ediam_image_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) (s : Set α) :
          theorem LipschitzWith.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) {x : α} {y : α} {d : ENNReal} (h : edist x y < d / K) :
          edist (f x) (f y) < d
          theorem LipschitzWith.uniformContinuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) :

          A Lipschitz function is uniformly continuous.

          theorem LipschitzWith.continuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) :

          A Lipschitz function is continuous.

          theorem LipschitzWith.const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :
          LipschitzWith 0 fun (x : α) => b

          Constant functions are Lipschitz (with any constant).

          theorem LipschitzWith.const' {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) {K : NNReal} :
          LipschitzWith K fun (x : α) => b

          The identity is 1-Lipschitz.

          theorem LipschitzWith.subtype_val {α : Type u} [PseudoEMetricSpace α] (s : Set α) :
          LipschitzWith 1 Subtype.val

          The inclusion of a subset is 1-Lipschitz.

          theorem LipschitzWith.subtype_mk {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) {p : βProp} (hp : ∀ (x : α), p (f x)) :
          LipschitzWith K fun (x : α) => f x,
          theorem LipschitzWith.eval {ι : Type x} {α : ιType u} [(i : ι) → PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) :
          theorem LipschitzWith.restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : αβ} (hf : LipschitzWith K f) (s : Set α) :
          LipschitzWith K (s.restrict f)

          The restriction of a K-Lipschitz function is K-Lipschitz.

          theorem LipschitzWith.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf : NNReal} {Kg : NNReal} {f : βγ} {g : αβ} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
          LipschitzWith (Kf * Kg) (f g)

          The composition of Lipschitz functions is Lipschitz.

          theorem LipschitzWith.comp_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {Kf : NNReal} {Kg : NNReal} {f : βγ} {g : αβ} {s : Set α} (hf : LipschitzWith Kf f) (hg : LipschitzOnWith Kg g s) :
          LipschitzOnWith (Kf * Kg) (f g) s
          theorem LipschitzWith.prod {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : αβ} {Kf : NNReal} (hf : LipschitzWith Kf f) {g : αγ} {Kg : NNReal} (hg : LipschitzWith Kg g) :
          LipschitzWith (max Kf Kg) fun (x : α) => (f x, g x)

          If f and g are Lipschitz functions, so is the induced map f × g to the product type.

          theorem LipschitzWith.prod_mk_right {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :
          LipschitzWith 1 fun (a : α) => (a, b)
          theorem LipschitzWith.uncurry {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : αβγ} {Kα : NNReal} {Kβ : NNReal} (hα : ∀ (b : β), LipschitzWith fun (a : α) => f a b) (hβ : ∀ (a : α), LipschitzWith (f a)) :
          theorem LipschitzWith.iterate {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : αα} (hf : LipschitzWith K f) (n : ) :

          Iterates of a Lipschitz function are Lipschitz.

          theorem LipschitzWith.edist_iterate_succ_le_geometric {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : αα} (hf : LipschitzWith K f) (x : α) (n : ) :
          edist (f^[n] x) (f^[n + 1] x) edist x (f x) * K ^ n
          theorem LipschitzWith.mul_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {g : Function.End α} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
          LipschitzWith (Kf * Kg) (f * g)
          theorem LipschitzWith.list_prod {α : Type u} {ι : Type x} [PseudoEMetricSpace α] (f : ιFunction.End α) (K : ιNNReal) (h : ∀ (i : ι), LipschitzWith (K i) (f i)) (l : List ι) :
          LipschitzWith (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 LipschitzWith.pow_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {K : NNReal} (h : LipschitzWith K f) (n : ) :
          LipschitzWith (K ^ n) (f ^ n)
          theorem LipschitzOnWith.uniformContinuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} (hf : LipschitzOnWith K f s) :
          theorem LipschitzOnWith.continuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} (hf : LipschitzOnWith K f s) :
          theorem LipschitzOnWith.edist_le_mul_of_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} (h : LipschitzOnWith K f s) {x : α} {y : α} (hx : x s) (hy : y s) {r : ENNReal} (hr : edist x y r) :
          edist (f x) (f y) K * r
          theorem LipschitzOnWith.edist_lt_of_edist_lt_div {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : αβ} (hf : LipschitzOnWith K f s) {x : α} {y : α} (hx : x s) (hy : y s) {d : ENNReal} (hd : edist x y < d / K) :
          edist (f x) (f y) < d
          theorem LipschitzOnWith.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {K : NNReal} {s : Set α} {f : αβ} {g : βγ} {t : Set β} {Kg : NNReal} (hg : LipschitzOnWith Kg g t) (hf : LipschitzOnWith K f s) (hmaps : Set.MapsTo f s t) :
          LipschitzOnWith (Kg * K) (g f) s
          theorem LipschitzOnWith.prod {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {s : Set α} {f : αβ} {g : αγ} {Kf : NNReal} {Kg : NNReal} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
          LipschitzOnWith (max Kf Kg) (fun (x : α) => (f x, g x)) s

          If f and g are Lipschitz on s, so is the induced map f × g to the product type.

          theorem LipschitzOnWith.ediam_image2_le {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : αβγ) {K₁ : NNReal} {K₂ : NNReal} (s : Set α) (t : Set β) (hf₁ : bt, LipschitzOnWith K₁ (fun (x : α) => f x b) s) (hf₂ : as, LipschitzOnWith K₂ (f a) t) :
          EMetric.diam (Set.image2 f s t) K₁ * EMetric.diam s + K₂ * EMetric.diam t
          theorem LipschitzWith.locallyLipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} {K : NNReal} (hf : LipschitzWith K f) :

          A Lipschitz function is locally Lipschitz.

          The identity function is locally Lipschitz.

          theorem LocallyLipschitz.const {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :
          LocallyLipschitz fun (x : α) => b

          Constant functions are locally Lipschitz.

          theorem LocallyLipschitz.continuous {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} (hf : LocallyLipschitz f) :

          A locally Lipschitz function is continuous. (The converse is false: for example, $x ↦ \sqrt{x}$ is continuous, but not locally Lipschitz at 0.)

          theorem LocallyLipschitz.comp {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : βγ} {g : αβ} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :

          The composition of locally Lipschitz functions is locally Lipschitz. -

          theorem LocallyLipschitz.prod {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {f : αβ} (hf : LocallyLipschitz f) {g : αγ} (hg : LocallyLipschitz g) :
          LocallyLipschitz fun (x : α) => (f x, g x)

          If f and g are locally Lipschitz, so is the induced map f × g to the product type.

          theorem LocallyLipschitz.prod_mk_right {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (b : β) :
          LocallyLipschitz fun (a : α) => (a, b)
          theorem LocallyLipschitz.iterate {α : Type u} [PseudoEMetricSpace α] {f : αα} (hf : LocallyLipschitz f) (n : ) :
          theorem LocallyLipschitzOn.continuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} {s : Set α} (hf : LocallyLipschitzOn s f) :
          theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × βγ) {s : Set α} {s' : Set α} {t : Set β} (hs' : s' s) (hss' : s closure s') (K : NNReal) (ha : as', ContinuousOn (fun (y : β) => f (a, y)) t) (hb : bt, LipschitzOnWith K (fun (x : α) => f (x, b)) s) :

          Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical fiber” {a} × t, a ∈ s, and is Lipschitz continuous on each “horizontal fiber” s × {b}, b ∈ t with the same Lipschitz constant K. Then it is continuous on s × t. Moreover, it suffices to require continuity on vertical fibers for a from a subset s' ⊆ s that is dense in s.

          The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

          theorem continuousOn_prod_of_continuousOn_lipschitzOnWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × βγ) {s : Set α} {t : Set β} (K : NNReal) (ha : as, ContinuousOn (fun (y : β) => f (a, y)) t) (hb : bt, LipschitzOnWith K (fun (x : α) => f (x, b)) s) :

          Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical fiber” {a} × t, a ∈ s, and is Lipschitz continuous on each “horizontal fiber” s × {b}, b ∈ t with the same Lipschitz constant K. Then it is continuous on s × t.

          The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

          theorem continuous_prod_of_dense_continuous_lipschitzWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × βγ) (K : NNReal) {s : Set α} (hs : Dense s) (ha : as, Continuous fun (y : β) => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun (x : α) => f (x, b)) :

          Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ for a : α from a dense set. Suppose that it is Lipschitz continuous on each “horizontal section” univ × {b}, b : β with the same Lipschitz constant K. Then it is continuous.

          The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.

          theorem continuous_prod_of_continuous_lipschitzWith {α : Type u} {β : Type v} {γ : Type w} [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × βγ) (K : NNReal) (ha : ∀ (a : α), Continuous fun (y : β) => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun (x : α) => f (x, b)) :

          Consider a function f : α × β → γ. Suppose that it is continuous on each “vertical section” {a} × univ, a : α, and is Lipschitz continuous on each “horizontal section” univ × {b}, b : β with the same Lipschitz constant K. Then it is continuous.

          The actual statement uses (Lipschitz) continuity of fun y ↦ f (a, y) and fun x ↦ f (x, b) instead of continuity of f on subsets of the product space.