Antilipschitz functions #
We say that a map f : α → β between two (extended) metric spaces is
AntilipschitzWith 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 conjunction 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
AntilipschitzWith
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(K : NNReal)
(f : α → β)
:
We say that f : α → β is AntilipschitzWith K if for any two points x, y we have
edist x y ≤ K * edist (f x) (f y).
Instances For
theorem
AntilipschitzWith.edist_lt_top
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(h : AntilipschitzWith K f)
(x : α)
(y : α)
:
theorem
AntilipschitzWith.edist_ne_top
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(h : AntilipschitzWith K f)
(x : α)
(y : α)
:
theorem
antilipschitzWith_iff_le_mul_nndist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
:
theorem
AntilipschitzWith.of_le_mul_nndist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
:
(∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)) → AntilipschitzWith K f
Alias of the reverse direction of antilipschitzWith_iff_le_mul_nndist.
theorem
AntilipschitzWith.le_mul_nndist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
:
AntilipschitzWith K f → ∀ (x y : α), nndist x y ≤ K * nndist (f x) (f y)
Alias of the forward direction of antilipschitzWith_iff_le_mul_nndist.
theorem
antilipschitzWith_iff_le_mul_dist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
:
theorem
AntilipschitzWith.of_le_mul_dist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
:
(∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)) → AntilipschitzWith K f
Alias of the reverse direction of antilipschitzWith_iff_le_mul_dist.
theorem
AntilipschitzWith.le_mul_dist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
:
AntilipschitzWith K f → ∀ (x y : α), dist x y ≤ ↑K * dist (f x) (f y)
Alias of the forward direction of antilipschitzWith_iff_le_mul_dist.
theorem
AntilipschitzWith.mul_le_nndist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(x : α)
(y : α)
:
theorem
AntilipschitzWith.mul_le_dist
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(x : α)
(y : α)
:
def
AntilipschitzWith.k
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(_hf : AntilipschitzWith K f)
:
Extract the constant from hf : AntilipschitzWith K f. This is useful, e.g.,
if K is given by a long formula, and we want to reuse this value.
Equations
- _hf.k = K
Instances For
theorem
AntilipschitzWith.injective
{α : Type u_4}
{β : Type u_5}
[EMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
:
theorem
AntilipschitzWith.mul_le_edist
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(x : α)
(y : α)
:
theorem
AntilipschitzWith.ediam_preimage_le
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(s : Set β)
:
EMetric.diam (f ⁻¹' s) ≤ ↑K * EMetric.diam s
theorem
AntilipschitzWith.le_mul_ediam_image
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(s : Set α)
:
EMetric.diam s ≤ ↑K * EMetric.diam (f '' s)
theorem
AntilipschitzWith.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
{Kg : NNReal}
{g : β → γ}
(hg : AntilipschitzWith Kg g)
{Kf : NNReal}
{f : α → β}
(hf : AntilipschitzWith Kf f)
:
AntilipschitzWith (Kf * Kg) (g ∘ f)
theorem
AntilipschitzWith.restrict
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(s : Set α)
:
AntilipschitzWith K (s.restrict f)
theorem
AntilipschitzWith.codRestrict
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
{s : Set β}
(hs : ∀ (x : α), f x ∈ s)
:
AntilipschitzWith K (Set.codRestrict f s hs)
theorem
AntilipschitzWith.to_rightInvOn'
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
{s : Set α}
(hf : AntilipschitzWith K (s.restrict f))
{g : β → α}
{t : Set β}
(g_maps : Set.MapsTo g t s)
(g_inv : Set.RightInvOn g f t)
:
LipschitzWith K (t.restrict g)
theorem
AntilipschitzWith.to_rightInvOn
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
{g : β → α}
{t : Set β}
(h : Set.RightInvOn g f t)
:
LipschitzWith K (t.restrict g)
theorem
AntilipschitzWith.to_rightInverse
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
{g : β → α}
(hg : Function.RightInverse g f)
:
LipschitzWith K g
theorem
AntilipschitzWith.comap_uniformity_le
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
:
Filter.comap (Prod.map f f) (uniformity β) ≤ uniformity α
theorem
AntilipschitzWith.uniformInducing
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(hfc : UniformContinuous f)
:
theorem
AntilipschitzWith.isUniformEmbedding
{α : Type u_4}
{β : Type u_5}
[EMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(hfc : UniformContinuous f)
:
@[deprecated AntilipschitzWith.isUniformEmbedding]
theorem
AntilipschitzWith.uniformEmbedding
{α : Type u_4}
{β : Type u_5}
[EMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
(hfc : UniformContinuous f)
:
Alias of AntilipschitzWith.isUniformEmbedding.
theorem
AntilipschitzWith.isComplete_range
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
[CompleteSpace α]
(hf : AntilipschitzWith K f)
(hfc : UniformContinuous f)
:
IsComplete (Set.range f)
theorem
AntilipschitzWith.isClosed_range
{α : Type u_4}
{β : Type u_5}
[PseudoEMetricSpace α]
[EMetricSpace β]
[CompleteSpace α]
{f : α → β}
{K : NNReal}
(hf : AntilipschitzWith K f)
(hfc : UniformContinuous f)
:
theorem
AntilipschitzWith.closedEmbedding
{α : Type u_4}
{β : Type u_5}
[EMetricSpace α]
[EMetricSpace β]
{K : NNReal}
{f : α → β}
[CompleteSpace α]
(hf : AntilipschitzWith K f)
(hfc : UniformContinuous f)
:
theorem
AntilipschitzWith.subtype_coe
{α : Type u_1}
[PseudoEMetricSpace α]
(s : Set α)
:
AntilipschitzWith 1 Subtype.val
theorem
AntilipschitzWith.of_subsingleton
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{f : α → β}
[Subsingleton α]
{K : NNReal}
:
theorem
AntilipschitzWith.subsingleton
{α : Type u_4}
{β : Type u_5}
[EMetricSpace α]
[PseudoEMetricSpace β]
{f : α → β}
(h : AntilipschitzWith 0 f)
:
If f : α → β is 0-antilipschitz, then α is a subsingleton.
theorem
AntilipschitzWith.isBounded_preimage
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
{s : Set β}
(hs : Bornology.IsBounded s)
:
Bornology.IsBounded (f ⁻¹' s)
theorem
AntilipschitzWith.tendsto_cobounded
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : AntilipschitzWith K f)
:
theorem
AntilipschitzWith.properSpace
{β : Type u_2}
[PseudoMetricSpace β]
{α : Type u_4}
[MetricSpace α]
{K : NNReal}
{f : α → β}
[ProperSpace α]
(hK : AntilipschitzWith K f)
(f_cont : Continuous f)
(hf : Function.Surjective f)
:
The image of a proper space under an expanding onto map is proper.
theorem
AntilipschitzWith.isBounded_of_image2_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[PseudoMetricSpace γ]
(f : α → β → γ)
{K₁ : NNReal}
(hf : ∀ (b : β), AntilipschitzWith K₁ fun (a : α) => f a b)
{s : Set α}
{t : Set β}
(hst : Bornology.IsBounded (Set.image2 f s t))
:
theorem
AntilipschitzWith.isBounded_of_image2_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[PseudoMetricSpace γ]
{f : α → β → γ}
{K₂ : NNReal}
(hf : ∀ (a : α), AntilipschitzWith K₂ (f a))
{s : Set α}
{t : Set β}
(hst : Bornology.IsBounded (Set.image2 f s t))
:
theorem
LipschitzWith.to_rightInverse
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{K : NNReal}
{f : α → β}
(hf : LipschitzWith K f)
{g : β → α}
(hg : Function.RightInverse g f)
:
theorem
LipschitzWith.properSpace
{α : Type u_1}
{β : Type u_2}
[PseudoMetricSpace α]
[MetricSpace β]
[ProperSpace β]
{K : NNReal}
{f : α ≃ₜ β}
(hK : LipschitzWith K ⇑f)
:
The preimage of a proper space under a Lipschitz homeomorphism is proper.