Lipschitz continuous functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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.
Main definitions and lemmas #
lipschitz_with K f: states thatfis Lipschitz with constantK : ℝ≥0lipschitz_on_with K f: states thatfis Lipschitz with constantK : ℝ≥0on a setslipschitz_with.uniform_continuous: a Lipschitz function is uniformly continuouslipschitz_on_with.uniform_continuous_on: a function which is Lipschitz on a set is uniformly continuous on that set.
Implementation notes #
The parameter K has type ℝ≥0. This way we avoid conjuction in the definition and have
coercions both to ℝ and ℝ≥0∞. Constructors whose names end with ' take K : ℝ as an
argument, and return lipschitz_with (real.to_nnreal K) f.
def
lipschitz_with
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(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
- lipschitz_with K f = ∀ (x y : α), has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y
theorem
lipschitz_with_iff_dist_le_mul
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
lipschitz_with K f ↔ ∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y
theorem
lipschitz_with.of_dist_le_mul
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
(∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y) → lipschitz_with K f
Alias of the reverse direction of lipschitz_with_iff_dist_le_mul.
theorem
lipschitz_with.dist_le_mul
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
lipschitz_with K f → ∀ (x y : α), has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y
Alias of the forward direction of lipschitz_with_iff_dist_le_mul.
def
lipschitz_on_with
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(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
- lipschitz_on_with K f s = ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y
@[simp]
theorem
lipschitz_on_with_empty
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(K : nnreal)
(f : α → β) :
lipschitz_on_with K f ∅
theorem
lipschitz_on_with.mono
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{s t : set α}
{f : α → β}
(hf : lipschitz_on_with K f t)
(h : s ⊆ t) :
lipschitz_on_with K f s
theorem
lipschitz_on_with_iff_dist_le_mul
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{s : set α}
{f : α → β} :
lipschitz_on_with K f s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y
theorem
lipschitz_on_with.dist_le_mul
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{s : set α}
{f : α → β} :
lipschitz_on_with K f s → ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y
Alias of the forward direction of lipschitz_on_with_iff_dist_le_mul.
theorem
lipschitz_on_with.of_dist_le_mul
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{s : set α}
{f : α → β} :
(∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ ↑K * has_dist.dist x y) → lipschitz_on_with K f s
Alias of the reverse direction of lipschitz_on_with_iff_dist_le_mul.
@[simp]
theorem
lipschitz_on_univ
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β} :
lipschitz_on_with K f set.univ ↔ lipschitz_with K f
theorem
lipschitz_on_with_iff_restrict
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{s : set α} :
lipschitz_on_with K f s ↔ lipschitz_with K (s.restrict f)
theorem
lipschitz_on_with.to_restrict
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{s : set α} :
lipschitz_on_with K f s → lipschitz_with K (s.restrict f)
Alias of the forward direction of lipschitz_on_with_iff_restrict.
theorem
maps_to.lipschitz_on_with_iff_restrict
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{s : set α}
{t : set β}
(h : set.maps_to f s t) :
lipschitz_on_with K f s ↔ lipschitz_with K (set.maps_to.restrict f s t h)
theorem
lipschitz_on_with.to_restrict_maps_to
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{s : set α}
{t : set β}
(h : set.maps_to f s t) :
lipschitz_on_with K f s → lipschitz_with K (set.maps_to.restrict f s t h)
Alias of the forward direction of maps_to.lipschitz_on_with_iff_restrict.
@[protected]
theorem
lipschitz_with.lipschitz_on_with
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(s : set α) :
lipschitz_on_with K f s
theorem
lipschitz_with.edist_le_mul
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(x y : α) :
has_edist.edist (f x) (f y) ≤ ↑K * has_edist.edist x y
theorem
lipschitz_with.edist_le_mul_of_le
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{x y : α}
{r : ennreal}
(h : lipschitz_with K f)
(hr : has_edist.edist x y ≤ r) :
has_edist.edist (f x) (f y) ≤ ↑K * r
theorem
lipschitz_with.edist_lt_mul_of_lt
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{x y : α}
{r : ennreal}
(h : lipschitz_with K f)
(hK : K ≠ 0)
(hr : has_edist.edist x y < r) :
has_edist.edist (f x) (f y) < ↑K * r
theorem
lipschitz_with.maps_to_emetric_closed_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(x : α)
(r : ennreal) :
set.maps_to f (emetric.closed_ball x r) (emetric.closed_ball (f x) (↑K * r))
theorem
lipschitz_with.maps_to_emetric_ball
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(hK : K ≠ 0)
(x : α)
(r : ennreal) :
set.maps_to f (emetric.ball x r) (emetric.ball (f x) (↑K * r))
theorem
lipschitz_with.edist_lt_top
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{x y : α}
(h : has_edist.edist x y ≠ ⊤) :
has_edist.edist (f x) (f y) < ⊤
theorem
lipschitz_with.mul_edist_le
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(h : lipschitz_with K f)
(x y : α) :
(↑K)⁻¹ * has_edist.edist (f x) (f y) ≤ has_edist.edist x y
@[protected]
theorem
lipschitz_with.of_edist_le
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : ∀ (x y : α), has_edist.edist (f x) (f y) ≤ has_edist.edist x y) :
lipschitz_with 1 f
@[protected]
theorem
lipschitz_with.weaken
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{K' : nnreal}
(h : K ≤ K') :
lipschitz_with K' f
theorem
lipschitz_with.ediam_image_le
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(s : set α) :
emetric.diam (f '' s) ≤ ↑K * emetric.diam s
theorem
lipschitz_with.edist_lt_of_edist_lt_div
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{x y : α}
{d : ennreal}
(h : has_edist.edist x y < d / ↑K) :
has_edist.edist (f x) (f y) < d
@[protected]
theorem
lipschitz_with.uniform_continuous
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f) :
A Lipschitz function is uniformly continuous
@[protected]
theorem
lipschitz_with.continuous
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f) :
A Lipschitz function is continuous
@[protected]
theorem
lipschitz_with.const
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(b : β) :
lipschitz_with 0 (λ (a : α), b)
@[protected]
@[protected]
@[protected]
theorem
lipschitz_with.subtype_mk
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{p : β → Prop}
(hp : ∀ (x : α), p (f x)) :
lipschitz_with K (λ (x : α), ⟨f x, _⟩)
@[protected]
theorem
lipschitz_with.eval
{ι : Type x}
{α : ι → Type u}
[Π (i : ι), pseudo_emetric_space (α i)]
[fintype ι]
(i : ι) :
lipschitz_with 1 (function.eval i)
@[protected]
theorem
lipschitz_with.restrict
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(s : set α) :
lipschitz_with K (s.restrict f)
@[protected]
theorem
lipschitz_with.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{Kf Kg : nnreal}
{f : β → γ}
{g : α → β}
(hf : lipschitz_with Kf f)
(hg : lipschitz_with Kg g) :
lipschitz_with (Kf * Kg) (f ∘ g)
theorem
lipschitz_with.comp_lipschitz_on_with
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{Kf Kg : nnreal}
{f : β → γ}
{g : α → β}
{s : set α}
(hf : lipschitz_with Kf f)
(hg : lipschitz_on_with Kg g s) :
lipschitz_on_with (Kf * Kg) (f ∘ g) s
@[protected]
theorem
lipschitz_with.prod_fst
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β] :
@[protected]
theorem
lipschitz_with.prod_snd
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β] :
@[protected]
theorem
lipschitz_with.prod
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{f : α → β}
{Kf : nnreal}
(hf : lipschitz_with Kf f)
{g : α → γ}
{Kg : nnreal}
(hg : lipschitz_with Kg g) :
lipschitz_with (linear_order.max Kf Kg) (λ (x : α), (f x, g x))
@[protected]
theorem
lipschitz_with.prod_mk_left
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(a : α) :
lipschitz_with 1 (prod.mk a)
@[protected]
theorem
lipschitz_with.prod_mk_right
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(b : β) :
lipschitz_with 1 (λ (a : α), (a, b))
@[protected]
theorem
lipschitz_with.uncurry
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{f : α → β → γ}
{Kα Kβ : nnreal}
(hα : ∀ (b : β), lipschitz_with Kα (λ (a : α), f a b))
(hβ : ∀ (a : α), lipschitz_with Kβ (f a)) :
lipschitz_with (Kα + Kβ) (function.uncurry f)
@[protected]
theorem
lipschitz_with.iterate
{α : Type u}
[pseudo_emetric_space α]
{K : nnreal}
{f : α → α}
(hf : lipschitz_with K f)
(n : ℕ) :
lipschitz_with (K ^ n) f^[n]
theorem
lipschitz_with.edist_iterate_succ_le_geometric
{α : Type u}
[pseudo_emetric_space α]
{K : nnreal}
{f : α → α}
(hf : lipschitz_with K f)
(x : α)
(n : ℕ) :
@[protected]
theorem
lipschitz_with.mul
{α : Type u}
[pseudo_emetric_space α]
{f g : function.End α}
{Kf Kg : nnreal}
(hf : lipschitz_with Kf f)
(hg : lipschitz_with Kg g) :
lipschitz_with (Kf * Kg) (f * g)
@[protected]
theorem
lipschitz_with.list_prod
{α : Type u}
{ι : Type x}
[pseudo_emetric_space α]
(f : ι → function.End α)
(K : ι → nnreal)
(h : ∀ (i : ι), lipschitz_with (K i) (f i))
(l : list ι) :
lipschitz_with (list.map K l).prod (list.map f l).prod
The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous endomorphism.
@[protected]
theorem
lipschitz_with.pow
{α : Type u}
[pseudo_emetric_space α]
{f : function.End α}
{K : nnreal}
(h : lipschitz_with K f)
(n : ℕ) :
lipschitz_with (K ^ n) (f ^ n)
@[protected]
theorem
lipschitz_with.of_dist_le'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{K : ℝ}
(h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ K * has_dist.dist x y) :
@[protected]
theorem
lipschitz_with.mk_one
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
(h : ∀ (x y : α), has_dist.dist (f x) (f y) ≤ has_dist.dist x y) :
lipschitz_with 1 f
@[protected]
theorem
lipschitz_with.of_le_add_mul'
{α : Type u}
[pseudo_metric_space α]
{f : α → ℝ}
(K : ℝ)
(h : ∀ (x y : α), f x ≤ f y + K * has_dist.dist x y) :
For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version
doesn't assume 0≤K.
@[protected]
theorem
lipschitz_with.of_le_add_mul
{α : Type u}
[pseudo_metric_space α]
{f : α → ℝ}
(K : nnreal)
(h : ∀ (x y : α), f x ≤ f y + ↑K * has_dist.dist x y) :
lipschitz_with K f
For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version
assumes 0≤K.
@[protected]
theorem
lipschitz_with.of_le_add
{α : Type u}
[pseudo_metric_space α]
{f : α → ℝ}
(h : ∀ (x y : α), f x ≤ f y + has_dist.dist x y) :
lipschitz_with 1 f
@[protected]
theorem
lipschitz_with.le_add_mul
{α : Type u}
[pseudo_metric_space α]
{f : α → ℝ}
{K : nnreal}
(h : lipschitz_with K f)
(x y : α) :
f x ≤ f y + ↑K * has_dist.dist x y
@[protected]
theorem
lipschitz_with.iff_le_add_mul
{α : Type u}
[pseudo_metric_space α]
{f : α → ℝ}
{K : nnreal} :
lipschitz_with K f ↔ ∀ (x y : α), f x ≤ f y + ↑K * has_dist.dist x y
theorem
lipschitz_with.nndist_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(x y : α) :
has_nndist.nndist (f x) (f y) ≤ K * has_nndist.nndist x y
theorem
lipschitz_with.dist_le_mul_of_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
{x y : α}
{r : ℝ}
(hf : lipschitz_with K f)
(hr : has_dist.dist x y ≤ r) :
has_dist.dist (f x) (f y) ≤ ↑K * r
theorem
lipschitz_with.maps_to_closed_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(x : α)
(r : ℝ) :
set.maps_to f (metric.closed_ball x r) (metric.closed_ball (f x) (↑K * r))
theorem
lipschitz_with.dist_lt_mul_of_lt
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
{x y : α}
{r : ℝ}
(hf : lipschitz_with K f)
(hK : K ≠ 0)
(hr : has_dist.dist x y < r) :
has_dist.dist (f x) (f y) < ↑K * r
theorem
lipschitz_with.maps_to_ball
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(hK : K ≠ 0)
(x : α)
(r : ℝ) :
set.maps_to f (metric.ball x r) (metric.ball (f x) (↑K * r))
def
lipschitz_with.to_locally_bounded_map
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
(f : α → β)
(hf : lipschitz_with K f) :
A Lipschitz continuous map is a locally bounded map.
Equations
@[simp]
theorem
lipschitz_with.coe_to_locally_bounded_map
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f) :
⇑(lipschitz_with.to_locally_bounded_map f hf) = f
theorem
lipschitz_with.comap_cobounded_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f) :
theorem
lipschitz_with.bounded_image
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{s : set α}
(hs : metric.bounded s) :
metric.bounded (f '' s)
theorem
lipschitz_with.diam_image_le
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
(s : set α)
(hs : metric.bounded s) :
metric.diam (f '' s) ≤ ↑K * metric.diam s
@[protected]
theorem
lipschitz_with.dist_left
{α : Type u}
[pseudo_metric_space α]
(y : α) :
lipschitz_with 1 (λ (x : α), has_dist.dist x y)
@[protected]
theorem
lipschitz_with.dist_right
{α : Type u}
[pseudo_metric_space α]
(x : α) :
lipschitz_with 1 (has_dist.dist x)
@[protected]
theorem
lipschitz_with.dist_iterate_succ_le_geometric
{α : Type u}
[pseudo_metric_space α]
{K : nnreal}
{f : α → α}
(hf : lipschitz_with K f)
(x : α)
(n : ℕ) :
@[protected]
theorem
lipschitz_with.max
{α : Type u}
[pseudo_emetric_space α]
{f g : α → ℝ}
{Kf Kg : nnreal}
(hf : lipschitz_with Kf f)
(hg : lipschitz_with Kg g) :
lipschitz_with (linear_order.max Kf Kg) (λ (x : α), linear_order.max (f x) (g x))
@[protected]
theorem
lipschitz_with.min
{α : Type u}
[pseudo_emetric_space α]
{f g : α → ℝ}
{Kf Kg : nnreal}
(hf : lipschitz_with Kf f)
(hg : lipschitz_with Kg g) :
lipschitz_with (linear_order.max Kf Kg) (λ (x : α), linear_order.min (f x) (g x))
theorem
lipschitz_with.max_const
{α : Type u}
[pseudo_emetric_space α]
{f : α → ℝ}
{Kf : nnreal}
(hf : lipschitz_with Kf f)
(a : ℝ) :
lipschitz_with Kf (λ (x : α), linear_order.max (f x) a)
theorem
lipschitz_with.const_max
{α : Type u}
[pseudo_emetric_space α]
{f : α → ℝ}
{Kf : nnreal}
(hf : lipschitz_with Kf f)
(a : ℝ) :
lipschitz_with Kf (λ (x : α), linear_order.max a (f x))
theorem
lipschitz_with.min_const
{α : Type u}
[pseudo_emetric_space α]
{f : α → ℝ}
{Kf : nnreal}
(hf : lipschitz_with Kf f)
(a : ℝ) :
lipschitz_with Kf (λ (x : α), linear_order.min (f x) a)
theorem
lipschitz_with.const_min
{α : Type u}
[pseudo_emetric_space α]
{f : α → ℝ}
{Kf : nnreal}
(hf : lipschitz_with Kf f)
(a : ℝ) :
lipschitz_with Kf (λ (x : α), linear_order.min a (f x))
@[protected]
theorem
metric.bounded.left_of_prod
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{t : set β}
(h : metric.bounded (s ×ˢ t))
(ht : t.nonempty) :
theorem
metric.bounded.right_of_prod
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{t : set β}
(h : metric.bounded (s ×ˢ t))
(hs : s.nonempty) :
theorem
metric.bounded_prod_of_nonempty
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{t : set β}
(hs : s.nonempty)
(ht : t.nonempty) :
metric.bounded (s ×ˢ t) ↔ metric.bounded s ∧ metric.bounded t
theorem
metric.bounded_prod
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{t : set β} :
metric.bounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ metric.bounded s ∧ metric.bounded t
@[protected]
theorem
lipschitz_on_with.uniform_continuous_on
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{s : set α}
{f : α → β}
(hf : lipschitz_on_with K f s) :
@[protected]
theorem
lipschitz_on_with.continuous_on
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{s : set α}
{f : α → β}
(hf : lipschitz_on_with K f s) :
continuous_on f s
theorem
lipschitz_on_with.edist_lt_of_edist_lt_div
{α : Type u}
{β : Type v}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{s : set α}
{f : α → β}
(hf : lipschitz_on_with K f s)
{x y : α}
(hx : x ∈ s)
(hy : y ∈ s)
{d : ennreal}
(hd : has_edist.edist x y < d / ↑K) :
has_edist.edist (f x) (f y) < d
@[protected]
theorem
lipschitz_on_with.comp
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{K : nnreal}
{s : set α}
{f : α → β}
{g : β → γ}
{t : set β}
{Kg : nnreal}
(hg : lipschitz_on_with Kg g t)
(hf : lipschitz_on_with K f s)
(hmaps : set.maps_to f s t) :
lipschitz_on_with (Kg * K) (g ∘ f) s
theorem
lipschitz_on_with.ediam_image2_le
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
(f : α → β → γ)
{K₁ K₂ : nnreal}
(s : set α)
(t : set β)
(hf₁ : ∀ (b : β), b ∈ t → lipschitz_on_with K₁ (λ (a : α), f a b) s)
(hf₂ : ∀ (a : α), a ∈ s → lipschitz_on_with K₂ (f a) t) :
emetric.diam (set.image2 f s t) ≤ ↑K₁ * emetric.diam s + ↑K₂ * emetric.diam t
@[protected]
theorem
lipschitz_on_with.of_dist_le'
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{f : α → β}
{K : ℝ}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ K * has_dist.dist x y) :
lipschitz_on_with K.to_nnreal f s
@[protected]
theorem
lipschitz_on_with.mk_one
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{s : set α}
{f : α → β}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → has_dist.dist (f x) (f y) ≤ has_dist.dist x y) :
lipschitz_on_with 1 f s
@[protected]
theorem
lipschitz_on_with.of_le_add_mul'
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{f : α → ℝ}
(K : ℝ)
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + K * has_dist.dist x y) :
lipschitz_on_with K.to_nnreal f s
For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version
doesn't assume 0≤K.
@[protected]
theorem
lipschitz_on_with.of_le_add_mul
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{f : α → ℝ}
(K : nnreal)
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + ↑K * has_dist.dist x y) :
lipschitz_on_with K f s
For functions to ℝ, it suffices to prove f x ≤ f y + K * dist x y; this version
assumes 0≤K.
@[protected]
theorem
lipschitz_on_with.of_le_add
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{f : α → ℝ}
(h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + has_dist.dist x y) :
lipschitz_on_with 1 f s
@[protected]
theorem
lipschitz_on_with.le_add_mul
{α : Type u}
[pseudo_metric_space α]
{s : set α}
{f : α → ℝ}
{K : nnreal}
(h : lipschitz_on_with K f s)
{x : α}
(hx : x ∈ s)
{y : α}
(hy : y ∈ s) :
f x ≤ f y + ↑K * has_dist.dist x y
theorem
lipschitz_on_with.bounded_image2
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_metric_space α]
[pseudo_metric_space β]
[pseudo_metric_space γ]
(f : α → β → γ)
{K₁ K₂ : nnreal}
{s : set α}
{t : set β}
(hs : metric.bounded s)
(ht : metric.bounded t)
(hf₁ : ∀ (b : β), b ∈ t → lipschitz_on_with K₁ (λ (a : α), f a b) s)
(hf₂ : ∀ (a : α), a ∈ s → lipschitz_on_with K₂ (f a) t) :
metric.bounded (set.image2 f s t)
theorem
continuous_on_prod_of_continuous_on_lipschitz_on
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[topological_space β]
[pseudo_emetric_space γ]
(f : α × β → γ)
{s : set α}
{t : set β}
(K : nnreal)
(ha : ∀ (a : α), a ∈ s → continuous_on (λ (y : β), f (a, y)) t)
(hb : ∀ (b : β), b ∈ t → lipschitz_on_with K (λ (x : α), f (x, b)) s) :
continuous_on 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 λ y, f (a, y) and λ x, f (x, b) instead
of continuity of f on subsets of the product space.
theorem
continuous_prod_of_continuous_lipschitz
{α : Type u}
{β : Type v}
{γ : Type w}
[pseudo_emetric_space α]
[topological_space β]
[pseudo_emetric_space γ]
(f : α × β → γ)
(K : nnreal)
(ha : ∀ (a : α), continuous (λ (y : β), f (a, y)))
(hb : ∀ (b : β), lipschitz_with K (λ (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 λ y, f (a, y) and λ x, f (x, b) instead
of continuity of f on subsets of the product space.
theorem
continuous_at_of_locally_lipschitz
{α : Type u}
{β : Type v}
[pseudo_metric_space α]
[pseudo_metric_space β]
{f : α → β}
{x : α}
{r : ℝ}
(hr : 0 < r)
(K : ℝ)
(h : ∀ (y : α), has_dist.dist y x < r → has_dist.dist (f y) (f x) ≤ K * has_dist.dist y x) :
continuous_at f x
If a function is locally Lipschitz around a point, then it is continuous at this point.
theorem
lipschitz_on_with.extend_real
{α : Type u}
[pseudo_metric_space α]
{f : α → ℝ}
{s : set α}
{K : nnreal}
(hf : lipschitz_on_with K f s) :
A function f : α → ℝ which is K-Lipschitz on a subset s admits a K-Lipschitz extension
to the whole space.
theorem
lipschitz_on_with.extend_pi
{α : Type u}
{ι : Type x}
[pseudo_metric_space α]
[fintype ι]
{f : α → ι → ℝ}
{s : set α}
{K : nnreal}
(hf : lipschitz_on_with K f s) :
A function f : α → (ι → ℝ) which is K-Lipschitz on a subset s admits a K-Lipschitz
extension to the whole space.
TODO: state the same result (with the same proof) for the space ℓ^∞ (ι, ℝ) over a possibly
infinite type ι.