# mathlib3documentation

topology.metric_space.dilation

# Dilations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 defintions #

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

## 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 choosen 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 pseudo_emetric_space and we specialize to pseudo_metric_space and metric_space when needed.

## TODO #

• Introduce dilation equivs.
• Refactor the isometry API to match the *_hom_class API below.

## References #

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.

Instances for dilation
@[class]
structure dilation_class (F : Type u_3) (α : out_param (Type u_4)) (β : out_param (Type u_5))  :
Type (max u_3 u_4 u_5)

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

Instances of this typeclass
Instances of other typeclasses for dilation_class
• dilation_class.has_sizeof_inst
@[protected, instance]
def dilation.to_dilation_class {α : Type u_1} {β : Type u_2}  :
dilation_class (dilation α β) α β
Equations
@[protected, instance]
def dilation.has_coe_to_fun {α : Type u_1} {β : Type u_2}  :
has_coe_to_fun (dilation α β) (λ (_x : β), α β)
Equations
@[simp]
theorem dilation.to_fun_eq_coe {α : Type u_1} {β : Type u_2} {f : β} :
@[simp]
theorem dilation.coe_mk {α : Type u_1} {β : Type u_2} (f : α β) (h : (r : nnreal), r 0 (x y : α), has_edist.edist (f x) (f y) = r * ) :
{to_fun := 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
@[ext]
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 : α), has_edist.edist (f x) (f y) = r * ) :
{to_fun := f, edist_eq' := h} = f
@[simp]
theorem dilation.copy_to_fun {α : Type u_1} {β : Type u_2} (f : β) (f' : α β) (h : f' = f) :
(f.copy f' h) = f'
@[protected]
def dilation.copy {α : Type u_1} {β : Type u_2} (f : β) (f' : α β) (h : f' = f) :
β

Copy of a dilation with a new to_fun equal to the old one. Useful to fix definitional equalities.

Equations
theorem dilation.copy_eq_self {α : Type u_1} {β : Type u_2} (f : β) {f' : α β} (h : f' = f) :
f.copy f' h = f
noncomputable def dilation.ratio {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (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
theorem dilation.ratio_ne_zero {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :
theorem dilation.ratio_pos {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :
@[simp]
theorem dilation.edist_eq {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (x y : α) :
@[simp]
theorem dilation.nndist_eq {α : Type u_1} {β : Type u_2} {F : Type u_3} [ β] (f : F) (x y : α) :
@[simp]
theorem dilation.dist_eq {α : Type u_1} {β : Type u_2} {F : Type u_3} [ β] (f : F) (x y : α) :
has_dist.dist (f x) (f y) = *
theorem dilation.ratio_unique {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] {f : F} {x y : α} {r : nnreal} (h₀ : 0) (htop : ) (hr : has_edist.edist (f x) (f y) = r * ) :

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_1} {β : Type u_2} {F : Type u_3} [ β] {f : F} {x y : α} {r : nnreal} (hxy : 0) (hr : has_nndist.nndist (f x) (f y) = r * ) :

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_1} {β : Type u_2} {F : Type u_3} [ β] {f : F} {x y : α} {r : nnreal} (hxy : 0) (hr : has_dist.dist (f x) (f y) = r * ) :

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

def dilation.mk_of_nndist_eq {α : Type u_1} {β : Type u_2} (f : α β) (h : (r : nnreal), r 0 (x y : α), has_nndist.nndist (f x) (f y) = r * ) :
β

Alternative dilation constructor when the distance hypothesis is over nndist

Equations
@[simp]
theorem dilation.coe_mk_of_nndist_eq {α : Type u_1} {β : Type u_2} (f : α β) (h : (r : nnreal), r 0 (x y : α), has_nndist.nndist (f x) (f y) = r * ) :
= f
@[simp]
theorem dilation.mk_coe_of_nndist_eq {α : Type u_1} {β : Type u_2} (f : β) (h : (r : nnreal), r 0 (x y : α), has_nndist.nndist (f x) (f y) = r * ) :
def dilation.mk_of_dist_eq {α : Type u_1} {β : Type u_2} (f : α β) (h : (r : nnreal), r 0 (x y : α), has_dist.dist (f x) (f y) = r * ) :
β

Alternative dilation constructor when the distance hypothesis is over dist

Equations
@[simp]
theorem dilation.coe_mk_of_dist_eq {α : Type u_1} {β : Type u_2} (f : α β) (h : (r : nnreal), r 0 (x y : α), has_dist.dist (f x) (f y) = r * ) :
= f
@[simp]
theorem dilation.mk_coe_of_dist_eq {α : Type u_1} {β : Type u_2} (f : β) (h : (r : nnreal), r 0 (x y : α), has_dist.dist (f x) (f y) = r * ) :
theorem dilation.lipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :
theorem dilation.antilipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :
@[protected]
theorem dilation.injective {β : Type u_2} {F : Type u_4} {α : Type u_1} [ β] (f : F) :

A dilation from an emetric space is injective

@[protected]
def dilation.id (α : Type u_1)  :
α

The identity is a dilation

Equations
@[protected, instance]
def dilation.inhabited {α : Type u_1}  :
Equations
@[protected, simp]
theorem dilation.coe_id {α : Type u_1}  :
theorem dilation.id_ratio {α : 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
theorem dilation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (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)
@[simp]
theorem dilation.comp_ratio {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ} {f : β} (hne : (x y : α), 0 ) :

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

@[simp]
theorem dilation.comp_id {α : Type u_1} {β : Type u_2} (f : β) :
f.comp (dilation.id α) = f
@[simp]
theorem dilation.id_comp {α : Type u_1} {β : Type u_2} (f : β) :
(dilation.id β).comp f = f
@[protected, instance]
def dilation.monoid {α : Type u_1}  :
Equations
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}  :
@[simp]
theorem dilation.coe_mul {α : Type u_1} (f g : α) :
(f * g) = f g
theorem dilation.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g₁ g₂ : γ} {f : β} (hf : function.surjective f) :
g₁.comp f = g₂.comp f g₁ = g₂
theorem dilation.cancel_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ} {f₁ f₂ : β} (hg : function.injective g) :
g.comp f₁ = g.comp f₂ f₁ = f₂
@[protected]
theorem dilation.uniform_inducing {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (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} [ β] (f : F) {ι : Type u_3} {g : ι α} {a : filter ι} {b : α} :
(nhds b) filter.tendsto (f g) a (nhds (f b))
theorem dilation.to_continuous {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :

A dilation is continuous.

theorem dilation.ediam_image {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (s : set α) :

Dilations scale the diameter by ratio f in pseudoemetric spaces.

theorem dilation.ediam_range {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :

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

theorem dilation.maps_to_emetric_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (x : α) (r : ennreal) :
r) (emetric.ball (f x) ( * r))

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

theorem dilation.maps_to_emetric_closed_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (x : α) (r' : ennreal) :
r') (emetric.closed_ball (f x) ( * r'))

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

theorem dilation.comp_continuous_on_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) {γ : Type u_3} {g : γ α} {s : set γ} :
theorem dilation.comp_continuous_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) {γ : Type u_3} {g : γ α} :
@[protected]
theorem dilation.uniform_embedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :

A dilation from a metric space is a uniform embedding

@[protected]
theorem dilation.embedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :

A dilation from a metric space is an embedding

@[protected]
theorem dilation.closed_embedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) :

A dilation from a complete emetric space is a closed embedding

theorem dilation.diam_image {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (s : set α) :

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} [ β] (f : F) :
theorem dilation.maps_to_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (x : α) (r' : ) :
r') (metric.ball (f x) ( * r'))

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

theorem dilation.maps_to_sphere {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (x : α) (r' : ) :
r') (metric.sphere (f x) ( * r'))

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

theorem dilation.maps_to_closed_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [ β] (f : F) (x : α) (r' : ) :
r') (metric.closed_ball (f x) ( * r'))

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