Antilipschitz functions
We say that a map f : α → β between two (extended) metric spaces is
antilipschitz_with K, K ≥ 0, if for all x, y we have edist x y ≤ K * edist (f x) (f y).
For a metric space, the latter inequality is equivalent to dist x y ≤ K * dist (f x) (f y).
Implementation notes
The parameter K has type nnreal. This way we avoid conjuction in the definition and have
coercions both to ℝ and ennreal. We do not require 0 < K in the definition, mostly because
we do not have a posreal type.
def
antilipschitz_with
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
(K : ℝ≥0)
(f : α → β) :
Prop
We say that f : α → β is antilipschitz_with K if for any two points x, y we have
K * edist x y ≤ edist (f x) (f y).
theorem
antilipschitz_with_iff_le_mul_dist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[metric_space β]
{K : ℝ≥0}
{f : α → β} :
theorem
antilipschitz_with.mul_le_dist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[metric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
(x y : α) :
@[nolint]
def
antilipschitz_with.K
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f) :
Extract the constant from hf : antilipschitz_with K f. This is useful, e.g.,
if K is given by a long formula, and we want to reuse this value.
theorem
antilipschitz_with.injective
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f) :
theorem
antilipschitz_with.mul_le_edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
(x y : α) :
theorem
antilipschitz_with.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[emetric_space α]
[emetric_space β]
[emetric_space γ]
{Kg : ℝ≥0}
{g : β → γ}
(hg : antilipschitz_with Kg g)
{Kf : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with Kf f) :
antilipschitz_with (Kf * Kg) (g ∘ f)
theorem
antilipschitz_with.restrict
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
(s : set α) :
antilipschitz_with K (set.restrict f s)
theorem
antilipschitz_with.cod_restrict
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
{s : set β}
(hs : ∀ (x : α), f x ∈ s) :
antilipschitz_with K (set.cod_restrict f s hs)
theorem
antilipschitz_with.to_right_inv_on'
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
{s : set α}
(hf : antilipschitz_with K (set.restrict f s))
{g : β → α}
{t : set β}
(g_maps : set.maps_to g t s)
(g_inv : set.right_inv_on g f t) :
lipschitz_with K (set.restrict g t)
theorem
antilipschitz_with.to_right_inv_on
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
{g : β → α}
{t : set β}
(h : set.right_inv_on g f t) :
lipschitz_with K (set.restrict g t)
theorem
antilipschitz_with.to_right_inverse
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
{g : β → α}
(hg : function.right_inverse g f) :
lipschitz_with K g
theorem
antilipschitz_with.uniform_embedding
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : antilipschitz_with K f)
(hfc : uniform_continuous f) :
theorem
antilipschitz_with.of_subsingleton
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{f : α → β}
[subsingleton α]
{K : ℝ≥0} :
theorem
lipschitz_with.to_right_inverse
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : ℝ≥0}
{f : α → β}
(hf : lipschitz_with K f)
{g : β → α}
(hg : function.right_inverse g f) :