Antilipschitz functions #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 ℝ≥0. This way we avoid conjuction in the definition and have
coercions both to ℝ and ℝ≥0∞. 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}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
(K : nnreal)
(f : α → β) :
Prop
We say that f : α → β is antilipschitz_with K if for any two points x, y we have
edist x y ≤ K * 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.edist_lt_top
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(h : antilipschitz_with K f)
(x y : α) :
has_edist.edist x y < ⊤
theorem
antilipschitz_with.edist_ne_top
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(h : antilipschitz_with K f)
(x y : α) :
has_edist.edist x y ≠ ⊤
theorem
antilipschitz_with_iff_le_mul_nndist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
antilipschitz_with K f ↔ ∀ (x y : α), has_nndist.nndist x y ≤ K * has_nndist.nndist (f x) (f y)
theorem
antilipschitz_with.le_mul_nndist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
antilipschitz_with K f → ∀ (x y : α), has_nndist.nndist x y ≤ K * has_nndist.nndist (f x) (f y)
Alias of the forward direction of antilipschitz_with_iff_le_mul_nndist.
theorem
antilipschitz_with.of_le_mul_nndist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
(∀ (x y : α), has_nndist.nndist x y ≤ K * has_nndist.nndist (f x) (f y)) → antilipschitz_with K f
Alias of the reverse direction of antilipschitz_with_iff_le_mul_nndist.
theorem
antilipschitz_with_iff_le_mul_dist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_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.le_mul_dist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
antilipschitz_with K f → ∀ (x y : α), has_dist.dist x y ≤ ↑K * has_dist.dist (f x) (f y)
Alias of the forward direction of antilipschitz_with_iff_le_mul_dist.
theorem
antilipschitz_with.of_le_mul_dist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β} :
(∀ (x y : α), has_dist.dist x y ≤ ↑K * has_dist.dist (f x) (f y)) → antilipschitz_with K f
Alias of the reverse direction of antilipschitz_with_iff_le_mul_dist.
theorem
antilipschitz_with.mul_le_nndist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(x y : α) :
K⁻¹ * has_nndist.nndist x y ≤ has_nndist.nndist (f x) (f y)
theorem
antilipschitz_with.mul_le_dist
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_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)
@[protected, nolint]
def
antilipschitz_with.K
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{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.
@[protected]
theorem
antilipschitz_with.injective
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f) :
theorem
antilipschitz_with.mul_le_edist
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_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.ediam_preimage_le
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(s : set β) :
emetric.diam (f ⁻¹' s) ≤ ↑K * emetric.diam s
theorem
antilipschitz_with.le_mul_ediam_image
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(s : set α) :
emetric.diam s ≤ ↑K * emetric.diam (f '' s)
@[protected]
theorem
antilipschitz_with.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
[pseudo_emetric_space γ]
{Kg : nnreal}
{g : β → γ}
(hg : antilipschitz_with Kg g)
{Kf : nnreal}
{f : α → β}
(hf : antilipschitz_with Kf f) :
antilipschitz_with (Kf * Kg) (g ∘ f)
theorem
antilipschitz_with.restrict
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(s : set α) :
antilipschitz_with K (s.restrict f)
theorem
antilipschitz_with.cod_restrict
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_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}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
{s : set α}
(hf : antilipschitz_with K (s.restrict f))
{g : β → α}
{t : set β}
(g_maps : set.maps_to g t s)
(g_inv : set.right_inv_on g f t) :
lipschitz_with K (t.restrict g)
theorem
antilipschitz_with.to_right_inv_on
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
{g : β → α}
{t : set β}
(h : set.right_inv_on g f t) :
lipschitz_with K (t.restrict g)
theorem
antilipschitz_with.to_right_inverse
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
{g : β → α}
(hg : function.right_inverse g f) :
lipschitz_with K g
theorem
antilipschitz_with.comap_uniformity_le
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f) :
filter.comap (prod.map f f) (uniformity β) ≤ uniformity α
@[protected]
theorem
antilipschitz_with.uniform_inducing
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(hfc : uniform_continuous f) :
@[protected]
theorem
antilipschitz_with.uniform_embedding
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
(hfc : uniform_continuous f) :
theorem
antilipschitz_with.is_complete_range
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
[complete_space α]
(hf : antilipschitz_with K f)
(hfc : uniform_continuous f) :
is_complete (set.range f)
theorem
antilipschitz_with.is_closed_range
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[emetric_space β]
[complete_space α]
{f : α → β}
{K : nnreal}
(hf : antilipschitz_with K f)
(hfc : uniform_continuous f) :
theorem
antilipschitz_with.closed_embedding
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[emetric_space β]
{K : nnreal}
{f : α → β}
[complete_space α]
(hf : antilipschitz_with K f)
(hfc : uniform_continuous f) :
theorem
antilipschitz_with.of_subsingleton
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
[subsingleton α]
{K : nnreal} :
@[protected]
theorem
antilipschitz_with.subsingleton
{α : Type u_1}
{β : Type u_2}
[emetric_space α]
[pseudo_emetric_space β]
{f : α → β}
(h : antilipschitz_with 0 f) :
If f : α → β is 0-antilipschitz, then α is a subsingleton.
theorem
antilipschitz_with.bounded_preimage
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f)
{s : set β}
(hs : metric.bounded s) :
metric.bounded (f ⁻¹' s)
theorem
antilipschitz_with.tendsto_cobounded
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[pseudo_metric_space β]
{K : nnreal}
{f : α → β}
(hf : antilipschitz_with K f) :
@[protected]
theorem
antilipschitz_with.proper_space
{β : Type u_2}
[pseudo_metric_space β]
{α : Type u_1}
[metric_space α]
{K : nnreal}
{f : α → β}
[proper_space α]
(hK : antilipschitz_with K f)
(f_cont : continuous f)
(hf : function.surjective f) :
The image of a proper space under an expanding onto map is proper.
theorem
antilipschitz_with.bounded_of_image2_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[pseudo_metric_space α]
[pseudo_metric_space β]
[pseudo_metric_space γ]
(f : α → β → γ)
{K₁ : nnreal}
(hf : ∀ (b : β), antilipschitz_with K₁ (λ (a : α), f a b))
{s : set α}
{t : set β}
(hst : metric.bounded (set.image2 f s t)) :
theorem
antilipschitz_with.bounded_of_image2_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[pseudo_metric_space α]
[pseudo_metric_space β]
[pseudo_metric_space γ]
{f : α → β → γ}
{K₂ : nnreal}
(hf : ∀ (a : α), antilipschitz_with K₂ (f a))
{s : set α}
{t : set β}
(hst : metric.bounded (set.image2 f s t)) :
theorem
lipschitz_with.to_right_inverse
{α : Type u_1}
{β : Type u_2}
[pseudo_emetric_space α]
[pseudo_emetric_space β]
{K : nnreal}
{f : α → β}
(hf : lipschitz_with K f)
{g : β → α}
(hg : function.right_inverse g f) :
@[protected]
theorem
lipschitz_with.proper_space
{α : Type u_1}
{β : Type u_2}
[pseudo_metric_space α]
[metric_space β]
[proper_space β]
{K : nnreal}
{f : α ≃ₜ β}
(hK : lipschitz_with K ⇑f) :
The preimage of a proper space under a Lipschitz homeomorphism is proper.