Dilations #

We define dilations, i.e., maps between emetric spaces that satisfy edist (f x) (f y) = r * edist x y for some r ∉ {0, ∞}.

The value r = 0 is not allowed because we want dilations of (e)metric spaces to be automatically injective. The value r = ∞ is not allowed because this way we can define Dilation.ratio f : ℝ≥0, not Dilation.ratio f : ℝ≥0∞. Also, we do not often need maps sending distinct points to points at infinite distance.

Main definitions #

• Dilation.ratio f : ℝ≥0: the value of r in the relation above, defaulting to 1 in the case where it is not well-defined.

Notation #

• α →ᵈ β: notation for Dilation α β.

Implementation notes #

The type of dilations defined in this file are also referred to as "similarities" or "similitudes" by other authors. The name Dilation was chosen to match the Wikipedia name.

Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the theory for PseudoEMetricSpace and we specialize to PseudoMetricSpace and MetricSpace when needed.

TODO #

• Introduce dilation equivs.
• Refactor the Isometry API to match the *HomClass API below.

References #

• https://en.wikipedia.org/wiki/Dilation_(metric_space)
• [Marcel Berger, Geometry][berger1987]
structure Dilation (α : Type u_1) (β : Type u_2) :
Type (max u_1 u_2)

A dilation is a map that uniformly scales the edistance between any two points.

• toFun : αβ
• edist_eq' : ∃ (r : NNReal), r 0 ∀ (x y : α), edist (self.toFun x) (self.toFun y) = r * edist x y
Instances For
theorem Dilation.edist_eq' {α : Type u_1} {β : Type u_2} (self : α →ᵈ β) :
∃ (r : NNReal), r 0 ∀ (x y : α), edist (self.toFun x) (self.toFun y) = r * edist x y
Equations
Instances For
class DilationClass (F : Type u_3) (α : Type u_4) (β : Type u_5) [FunLike F α β] :

DilationClass F α β r states that F is a type of r-dilations. You should extend this typeclass when you extend Dilation.

Instances
theorem DilationClass.edist_eq' {F : Type u_3} {α : Type u_4} {β : Type u_5} [FunLike F α β] [self : ] (f : F) :
∃ (r : NNReal), r 0 ∀ (x y : α), edist (f x) (f y) = r * edist x y
instance Dilation.funLike {α : Type u_1} {β : Type u_2} :
FunLike (α →ᵈ β) α β
Equations
• Dilation.funLike = { coe := Dilation.toFun, coe_injective' := }
instance Dilation.toDilationClass {α : Type u_1} {β : Type u_2} :
DilationClass (α →ᵈ β) α β
Equations
• =
instance Dilation.instCoeFunForall {α : Type u_1} {β : Type u_2} :
CoeFun (α →ᵈ β) fun (x : α →ᵈ β) => αβ
Equations
• Dilation.instCoeFunForall = DFunLike.hasCoeToFun
@[simp]
theorem Dilation.toFun_eq_coe {α : Type u_1} {β : Type u_2} {f : α →ᵈ β} :
f.toFun = f
@[simp]
theorem Dilation.coe_mk {α : Type u_1} {β : Type u_2} (f : αβ) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), edist (f x) (f y) = r * edist x y) :
{ toFun := f, edist_eq' := h } = f
theorem Dilation.congr_fun {α : Type u_1} {β : Type u_2} {f : α →ᵈ β} {g : α →ᵈ β} (h : f = g) (x : α) :
f x = g x
theorem Dilation.congr_arg {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) {x : α} {y : α} (h : x = y) :
f x = f y
theorem Dilation.ext {α : Type u_1} {β : Type u_2} {f : α →ᵈ β} {g : α →ᵈ β} (h : ∀ (x : α), f x = g x) :
f = g
theorem Dilation.ext_iff {α : Type u_1} {β : Type u_2} {f : α →ᵈ β} {g : α →ᵈ β} :
f = g ∀ (x : α), f x = g x
@[simp]
theorem Dilation.mk_coe {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), edist (f x) (f y) = r * edist x y) :
{ toFun := f, edist_eq' := h } = f
@[simp]
theorem Dilation.copy_toFun {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) (f' : αβ) (h : f' = f) :
(f.copy f' h) = f'
def Dilation.copy {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) (f' : αβ) (h : f' = f) :
α →ᵈ β

Copy of a Dilation with a new toFun equal to the old one. Useful to fix definitional equalities.

Equations
• f.copy f' h = { toFun := f', edist_eq' := }
Instances For
theorem Dilation.copy_eq_self {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) {f' : αβ} (h : f' = f) :
f.copy f' h = f
def Dilation.ratio {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :

The ratio of a dilation f. If the ratio is undefined (i.e., the distance between any two points in α is either zero or infinity), then we choose one as the ratio.

Equations
Instances For
theorem Dilation.ratio_of_trivial {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (h : ∀ (x y : α), edist x y = 0 edist x y = ) :
theorem Dilation.ratio_of_subsingleton {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] [] (f : F) :
theorem Dilation.ratio_ne_zero {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
theorem Dilation.ratio_pos {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
@[simp]
theorem Dilation.edist_eq {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (x : α) (y : α) :
edist (f x) (f y) = () * edist x y
@[simp]
theorem Dilation.nndist_eq {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [] (f : F) (x : α) (y : α) :
nndist (f x) (f y) = * nndist x y
@[simp]
theorem Dilation.dist_eq {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [] (f : F) (x : α) (y : α) :
dist (f x) (f y) = () * dist x y
theorem Dilation.ratio_unique {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] {f : F} {x : α} {y : α} {r : NNReal} (h₀ : edist x y 0) (htop : edist x y ) (hr : edist (f x) (f y) = r * edist x y) :

The ratio is equal to the distance ratio for any two points with nonzero finite distance. dist and nndist versions below

theorem Dilation.ratio_unique_of_nndist_ne_zero {α : Type u_6} {β : Type u_7} {F : Type u_8} [FunLike F α β] [] {f : F} {x : α} {y : α} {r : NNReal} (hxy : nndist x y 0) (hr : nndist (f x) (f y) = r * nndist x y) :

The ratio is equal to the distance ratio for any two points with nonzero finite distance; nndist version

theorem Dilation.ratio_unique_of_dist_ne_zero {α : Type u_7} {β : Type u_8} {F : Type u_6} [FunLike F α β] [] {f : F} {x : α} {y : α} {r : NNReal} (hxy : dist x y 0) (hr : dist (f x) (f y) = r * dist x y) :

The ratio is equal to the distance ratio for any two points with nonzero finite distance; dist version

def Dilation.mkOfNNDistEq {α : Type u_6} {β : Type u_7} (f : αβ) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) :
α →ᵈ β

Alternative Dilation constructor when the distance hypothesis is over nndist

Equations
• = { toFun := f, edist_eq' := }
Instances For
@[simp]
theorem Dilation.coe_mkOfNNDistEq {α : Type u_6} {β : Type u_7} (f : αβ) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) :
() = f
@[simp]
theorem Dilation.mk_coe_of_nndist_eq {α : Type u_6} {β : Type u_7} (f : α →ᵈ β) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), nndist (f x) (f y) = r * nndist x y) :
= f
def Dilation.mkOfDistEq {α : Type u_6} {β : Type u_7} (f : αβ) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), dist (f x) (f y) = r * dist x y) :
α →ᵈ β

Alternative Dilation constructor when the distance hypothesis is over dist

Equations
Instances For
@[simp]
theorem Dilation.coe_mkOfDistEq {α : Type u_6} {β : Type u_7} (f : αβ) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), dist (f x) (f y) = r * dist x y) :
() = f
@[simp]
theorem Dilation.mk_coe_of_dist_eq {α : Type u_6} {β : Type u_7} (f : α →ᵈ β) (h : ∃ (r : NNReal), r 0 ∀ (x y : α), dist (f x) (f y) = r * dist x y) :
@[simp]
theorem Isometry.toDilation_toFun {α : Type u_1} {β : Type u_2} (f : αβ) (hf : ) :
∀ (a : α), () a = f a
def Isometry.toDilation {α : Type u_1} {β : Type u_2} (f : αβ) (hf : ) :
α →ᵈ β

Every isometry is a dilation of ratio 1.

Equations
• = { toFun := f, edist_eq' := }
Instances For
@[simp]
theorem Isometry.toDilation_ratio {α : Type u_1} {β : Type u_2} {f : αβ} {hf : } :
= 1
theorem Dilation.lipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
theorem Dilation.antilipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
theorem Dilation.injective {β : Type u_2} {F : Type u_4} {α : Type u_6} [] [FunLike F α β] [] (f : F) :

A dilation from an emetric space is injective

def Dilation.id (α : Type u_6) :
α →ᵈ α

The identity is a dilation

Equations
• = { toFun := id, edist_eq' := }
Instances For
instance Dilation.instInhabited {α : Type u_1} :
Equations
• Dilation.instInhabited = { default := }
@[simp]
theorem Dilation.coe_id {α : Type u_1} :
() = id
theorem Dilation.ratio_id {α : Type u_1} :
def Dilation.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β →ᵈ γ) (f : α →ᵈ β) :
α →ᵈ γ

The composition of dilations is a dilation

Equations
• g.comp f = { toFun := g f, edist_eq' := }
Instances For
theorem Dilation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_6} (f : α →ᵈ β) (g : β →ᵈ γ) (h : γ →ᵈ δ) :
(h.comp g).comp f = h.comp (g.comp f)
@[simp]
theorem Dilation.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β →ᵈ γ) (f : α →ᵈ β) :
(g.comp f) = g f
theorem Dilation.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} (g : β →ᵈ γ) (f : α →ᵈ β) (x : α) :
(g.comp f) x = g (f x)
theorem Dilation.ratio_comp' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β →ᵈ γ} {f : α →ᵈ β} (hne : ∃ (x : α) (y : α), edist x y 0 edist x y ) :
Dilation.ratio (g.comp f) =

Ratio of the composition g.comp f of two dilations is the product of their ratios. We assume that there exist two points in α at extended distance neither 0 nor ∞ because otherwise Dilation.ratio (g.comp f) = Dilation.ratio f = 1 while Dilation.ratio g can be any number. This version works for most general spaces, see also Dilation.ratio_comp for a version assuming that α is a nontrivial metric space.

@[simp]
theorem Dilation.comp_id {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) :
f.comp () = f
@[simp]
theorem Dilation.id_comp {α : Type u_1} {β : Type u_2} (f : α →ᵈ β) :
().comp f = f
instance Dilation.instMonoid {α : Type u_1} :
Monoid (α →ᵈ α)
Equations
• Dilation.instMonoid = Monoid.mk npowRec
theorem Dilation.one_def {α : Type u_1} :
1 =
theorem Dilation.mul_def {α : Type u_1} (f : α →ᵈ α) (g : α →ᵈ α) :
f * g = f.comp g
@[simp]
theorem Dilation.coe_one {α : Type u_1} :
1 = id
@[simp]
theorem Dilation.coe_mul {α : Type u_1} (f : α →ᵈ α) (g : α →ᵈ α) :
(f * g) = f g
@[simp]
theorem Dilation.ratio_one {α : Type u_1} :
@[simp]
theorem Dilation.ratio_mul {α : Type u_1} (f : α →ᵈ α) (g : α →ᵈ α) :
@[simp]
theorem Dilation.ratioHom_apply {α : Type u_1} (f : α →ᵈ α) :
Dilation.ratioHom f =
def Dilation.ratioHom {α : Type u_1} :

Dilation.ratio as a monoid homomorphism from α →ᵈ α to ℝ≥0.

Equations
• Dilation.ratioHom = { toFun := Dilation.ratio, map_one' := , map_mul' := }
Instances For
@[simp]
theorem Dilation.ratio_pow {α : Type u_1} (f : α →ᵈ α) (n : ) :
@[simp]
theorem Dilation.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g₁ : β →ᵈ γ} {g₂ : β →ᵈ γ} {f : α →ᵈ β} (hf : ) :
g₁.comp f = g₂.comp f g₁ = g₂
@[simp]
theorem Dilation.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : β →ᵈ γ} {f₁ : α →ᵈ β} {f₂ : α →ᵈ β} (hg : ) :
g.comp f₁ = g.comp f₂ f₁ = f₂
theorem Dilation.uniformInducing {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :

A dilation from a metric space is a uniform inducing map

theorem Dilation.tendsto_nhds_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) {ι : Type u_6} {g : ια} {a : } {b : α} :
Filter.Tendsto g a (nhds b) Filter.Tendsto (f g) a (nhds (f b))
theorem Dilation.toContinuous {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :

A dilation is continuous.

theorem Dilation.ediam_image {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (s : Set α) :
EMetric.diam (f '' s) = () *

Dilations scale the diameter by ratio f in pseudoemetric spaces.

theorem Dilation.ediam_range {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
= () * EMetric.diam Set.univ

A dilation scales the diameter of the range by ratio f.

theorem Dilation.mapsTo_emetric_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (x : α) (r : ENNReal) :
Set.MapsTo (f) () (EMetric.ball (f x) (() * r))

A dilation maps balls to balls and scales the radius by ratio f.

theorem Dilation.mapsTo_emetric_closedBall {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (x : α) (r' : ENNReal) :
Set.MapsTo (f) () (EMetric.closedBall (f x) (() * r'))

A dilation maps closed balls to closed balls and scales the radius by ratio f.

theorem Dilation.comp_continuousOn_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) {γ : Type u_6} [] {g : γα} {s : Set γ} :
ContinuousOn (f g) s
theorem Dilation.comp_continuous_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) {γ : Type u_6} [] {g : γα} :
Continuous (f g)
theorem Dilation.uniformEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [] [FunLike F α β] [] (f : F) :

A dilation from a metric space is a uniform embedding

theorem Dilation.embedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [] [FunLike F α β] [] (f : F) :

A dilation from a metric space is an embedding

theorem Dilation.closedEmbedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [] [FunLike F α β] [] [] [] (f : F) :

A dilation from a complete emetric space is a closed embedding

@[simp]
theorem Dilation.ratio_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] {g : β →ᵈ γ} {f : α →ᵈ β} :
Dilation.ratio (g.comp f) =

Ratio of the composition g.comp f of two dilations is the product of their ratios. We assume that the domain α of f is a nontrivial metric space, otherwise Dilation.ratio f = Dilation.ratio (g.comp f) = 1 but Dilation.ratio g may have any value.

See also Dilation.ratio_comp' for a version that works for more general spaces.

theorem Dilation.diam_image {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (s : Set α) :
Metric.diam (f '' s) = () *

A dilation scales the diameter by ratio f in pseudometric spaces.

theorem Dilation.diam_range {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
Metric.diam () = () * Metric.diam Set.univ
theorem Dilation.mapsTo_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (x : α) (r' : ) :
Set.MapsTo (f) (Metric.ball x r') (Metric.ball (f x) (() * r'))

A dilation maps balls to balls and scales the radius by ratio f.

theorem Dilation.mapsTo_sphere {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (x : α) (r' : ) :
Set.MapsTo (f) () (Metric.sphere (f x) (() * r'))

A dilation maps spheres to spheres and scales the radius by ratio f.

theorem Dilation.mapsTo_closedBall {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) (x : α) (r' : ) :
Set.MapsTo (f) () (Metric.closedBall (f x) (() * r'))

A dilation maps closed balls to closed balls and scales the radius by ratio f.

theorem Dilation.tendsto_cobounded {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :
@[simp]
theorem Dilation.comap_cobounded {α : Type u_1} {β : Type u_2} {F : Type u_4} [FunLike F α β] [] (f : F) :