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 β] :
nnreal → (α → β) → 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).
Equations
- antilipschitz_with K f = ∀ (x y : α), has_edist.edist x y ≤ ↑K * has_edist.edist (f x) (f y)
theorem
antilipschitz_with_iff_le_mul_dist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[metric_space β]
{K : nnreal}
{f : α → β} :
antilipschitz_with K f ↔ ∀ (x y : α), has_dist.dist x y ≤ ↑K * has_dist.dist (f x) (f y)
theorem
antilipschitz_with.mul_le_dist
{α : Type u_1}
{β : Type u_2}
[metric_space α]
[metric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(x y : α) :
↑K⁻¹ * has_dist.dist x y ≤ has_dist.dist (f x) (f y)
@[nolint]
def
antilipschitz_with.K
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β} :
antilipschitz_with K f → nnreal
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 : nnreal}
{f : α → β} :
antilipschitz_with K f → function.injective f
theorem
antilipschitz_with.mul_le_edist
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(x y : α) :
↑K⁻¹ * has_edist.edist x y ≤ has_edist.edist (f x) (f y)
theorem
antilipschitz_with.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[emetric_space α]
[emetric_space β]
[emetric_space γ]
{Kg : nnreal}
{g : β → γ}
(hg : antilipschitz_with Kg g)
{Kf : nnreal}
{f : α → β} :
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 : nnreal}
{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 : nnreal}
{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 : nnreal}
{f : α → β}
{s : set α}
(hf : antilipschitz_with K (set.restrict f s))
{g : β → α}
{t : set β} :
set.maps_to g t s → 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 : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
{g : β → α}
{t : set β} :
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 : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
{g : β → α} :
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 : nnreal}
{f : α → β} :
antilipschitz_with K f → uniform_continuous f → uniform_embedding f
theorem
antilipschitz_with.of_subsingleton
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{f : α → β}
[subsingleton α]
{K : nnreal} :
theorem
lipschitz_with.to_right_inverse
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{g : β → α} :
function.right_inverse g f → antilipschitz_with K g