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

• LipschitzWith K f: states that f is Lipschitz with constant K : ℝ≥0
• LipschitzOnWith K f s: states that f is Lipschitz with constant K : ℝ≥0 on a set s
• LipschitzWith.uniformContinuous: a Lipschitz function is uniformly continuous
• LipschitzOnWith.uniformContinuousOn: a function which is Lipschitz on a set s is uniformly continuous on s.
• LocallyLipschitz f: states that f is locally Lipschitz
• LocallyLipschitz.continuous: a locally Lipschitz function is continuous.

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 : α → β) : 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

• LipschitzWith K f = ∀ (x y : α), edist (f x) (f y) ≤ ↑K * edist x y

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.

def LipschitzOnWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) (s : Set α) : Prop

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

• LipschitzOnWith K f s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → edist (f x) (f y) ≤ ↑K * edist x y

def LocallyLipschitz {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α → β) : Prop

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

Equations

• LocallyLipschitz f = ∀ (x : α), ∃ K t, t ∈ nhds x ∧ LipschitzOnWith K f t

@[simp]

theorem lipschitzOnWith_empty {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (K : NNReal) (f : α → β) : LipschitzOnWith K f ∅

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

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

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

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

Alias of the forward direction of lipschitzOnWith_iff_dist_le_mul.

@[simp]

theorem lipschitzOn_univ {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} : LipschitzOnWith K f Set.univ ↔ LipschitzWith K f

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

theorem lipschitzOnWith_iff_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} : LipschitzOnWith K f s ↔ LipschitzWith K (Set.restrict s f)

theorem LipschitzOnWith.to_restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} {s : Set α} : LipschitzOnWith K f s → LipschitzWith K (Set.restrict s f)

Alias of the forward direction of lipschitzOnWith_iff_restrict.

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

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

Alias of the forward direction of MapsTo.lipschitzOnWith_iff_restrict.

theorem LipschitzWith.lipschitzOnWith {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (h : LipschitzWith K f) (s : Set α) : LipschitzOnWith K f s

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) : Set.MapsTo f (EMetric.closedBall x r) (EMetric.closedBall (f x) (↑K * r))

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) : LipschitzWith 1 f

theorem LipschitzWith.weaken {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) {K' : NNReal} (h : K ≤ K') : LipschitzWith K' f

theorem LipschitzWith.ediam_image_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) : EMetric.diam (f '' s) ≤ ↑K * EMetric.diam s

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) : UniformContinuous f

A Lipschitz function is uniformly continuous.

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

theorem LipschitzWith.id {α : Type u} [PseudoEMetricSpace α] : LipschitzWith 1 id

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 => { val := f x, property := hp x }

theorem LipschitzWith.eval {ι : Type x} {α : ι → Type u} [(i : ι) → PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) : LipschitzWith 1 (Function.eval i)

theorem LipschitzWith.restrict {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : LipschitzWith K f) (s : Set α) : LipschitzWith K (Set.restrict s 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_fst {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith 1 Prod.fst

theorem LipschitzWith.prod_snd {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] : LipschitzWith 1 Prod.snd

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_left {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (a : α) : LipschitzWith 1 (Prod.mk a)

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 Kα fun a => f a b) (hβ : ∀ (a : α), LipschitzWith Kβ (f a)) : LipschitzWith (Kα + Kβ) (Function.uncurry f)

theorem LipschitzWith.iterate {α : Type u} [PseudoEMetricSpace α] {K : NNReal} {f : α → α} (hf : LipschitzWith K f) (n : ℕ) : LipschitzWith (K ^ n) 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.prod (List.map K l)) (List.prod (List.map f l))

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 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 (_ : ∀ (_s : Set α), Bornology.IsBounded _s → Bornology.IsBounded (f '' _s))

@[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.fst p.snd

theorem lipschitzWith_min : LipschitzWith 1 fun p => min p.fst p.snd

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.uniformContinuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) : UniformContinuousOn f s

theorem LipschitzOnWith.continuousOn {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} (hf : LipschitzOnWith K f s) : ContinuousOn f s

theorem LipschitzOnWith.edist_le_mul_of_le {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {s : Set α} {f : α → β} {x : α} {y : α} {r : ENNReal} (h : LipschitzOnWith K f s) (hx : x ∈ s) (hy : y ∈ s) (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.of_dist_le' {α : Type u} {β : Type v} [PseudoMetricSpace α] [PseudoMetricSpace β] {s : Set α} {f : α → β} {K : ℝ} (h : ∀ (x : α), x ∈ s → ∀ (y : α), 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 : α), x ∈ s → ∀ (y : α), 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 : α), x ∈ s → ∀ (y : α), 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 : α), x ∈ s → ∀ (y : α), 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 : α), x ∈ s → ∀ (y : α), 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 : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + ↑K * dist x y

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

A Lipschitz function is locally Lipschitz.

theorem LocallyLipschitz.id {α : Type u} [PseudoEMetricSpace α] : LocallyLipschitz id

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) : Continuous 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) : LocallyLipschitz (f ∘ 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_left {α : Type u} {β : Type v} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (a : α) : LocallyLipschitz (Prod.mk a)

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 : ℕ) : LocallyLipschitz f^[n]

theorem LocallyLipschitz.mul_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} {g : Function.End α} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (f * g)

theorem LocallyLipschitz.pow_end {α : Type u} [PseudoEMetricSpace α] {f : Function.End α} (h : LocallyLipschitz f) (n : ℕ) : LocallyLipschitz (f ^ n)

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 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 : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t) (hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)

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 : ∀ (a : α), a ∈ s → ContinuousOn (fun y => f (a, y)) t) (hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)

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 : ∀ (a : α), a ∈ s → Continuous fun y => f (a, y)) (hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)) : Continuous f

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)) : Continuous f

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.

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.