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 : α → β) : Prop

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).

Equations

• AntilipschitzWith K f = ∀ (x y : α), edist x y ≤ ↑K * edist (f x) (f y)

theorem AntilipschitzWith.edist_lt_top {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (h : AntilipschitzWith K f) (x : α) (y : α) : edist x y < ⊤

theorem AntilipschitzWith.edist_ne_top {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (h : AntilipschitzWith K f) (x : α) (y : α) : edist x y ≠ ⊤

theorem antilipschitzWith_iff_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)

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.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_iff_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)

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.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.mul_le_nndist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) (x : α) (y : α) : K⁻¹ * nndist x y ≤ nndist (f x) (f y)

theorem AntilipschitzWith.mul_le_dist {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) (x : α) (y : α) : ↑K⁻¹ * dist x y ≤ dist (f x) (f y)

def AntilipschitzWith.k {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (_hf : AntilipschitzWith K f) : NNReal

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

theorem AntilipschitzWith.injective {α : Type u_4} {β : Type u_5} [EMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) : Function.Injective f

theorem AntilipschitzWith.mul_le_edist {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) (x : α) (y : α) : (↑K)⁻¹ * edist x y ≤ edist (f x) (f 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.id {α : Type u_1} [PseudoEMetricSpace α] : AntilipschitzWith 1 id

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) : UniformInducing f

theorem AntilipschitzWith.uniformEmbedding {α : Type u_4} {β : Type u_5} [EMetricSpace α] [PseudoEMetricSpace β] {K : NNReal} {f : α → β} (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : UniformEmbedding f

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) : IsClosed (Set.range f)

theorem AntilipschitzWith.closedEmbedding {α : Type u_4} {β : Type u_5} [EMetricSpace α] [EMetricSpace β] {K : NNReal} {f : α → β} [CompleteSpace α] (hf : AntilipschitzWith K f) (hfc : UniformContinuous f) : ClosedEmbedding 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} : AntilipschitzWith K f

theorem AntilipschitzWith.subsingleton {α : Type u_4} {β : Type u_5} [EMetricSpace α] [PseudoEMetricSpace β] {f : α → β} (h : AntilipschitzWith 0 f) : Subsingleton α

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) : Filter.Tendsto f (Bornology.cobounded α) (Bornology.cobounded β)

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) : ProperSpace β

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)) : Bornology.IsBounded s ∨ Bornology.IsBounded 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)) : Bornology.IsBounded s ∨ Bornology.IsBounded 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) : AntilipschitzWith K g

theorem LipschitzWith.properSpace {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [MetricSpace β] [ProperSpace β] {K : NNReal} {f : α ≃ₜ β} (hK : LipschitzWith K ⇑f) : ProperSpace α

The preimage of a proper space under a Lipschitz homeomorphism is proper.