mathlib3 documentation

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 #

https://en.wikipedia.org/wiki/Dilation_(metric_space)
Marcel Berger, Geometry

structure dilation (α : Type u_1) (β : Type u_2) [pseudo_emetric_space α] [pseudo_emetric_space β] :

Type (max u_1 u_2)

to_fun : α → β
edist_eq' : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_edist.edist (self.to_fun x) (self.to_fun y) = ↑r * has_edist.edist x y

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)) [pseudo_emetric_space α] [pseudo_emetric_space β] :

Type (max u_3 u_4 u_5)

to_fun_like : fun_like F α (λ (_x : α), β)
edist_eq' : ∀ (f : F), ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_edist.edist (⇑f x) (⇑f y) = ↑r * has_edist.edist x y

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

dilation.to_dilation_class

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} [pseudo_emetric_space α] [pseudo_emetric_space β] :

dilation_class (dilation α β) α β

Equations

dilation.to_dilation_class = {to_fun_like := {coe := dilation.to_fun _inst_2, coe_injective' := _}, edist_eq' := _}

@[protected, instance]

def dilation.has_coe_to_fun {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] :

has_coe_to_fun (dilation α β) (λ (_x : dilation α β), α → β)

Equations

dilation.has_coe_to_fun = fun_like.has_coe_to_fun

@[simp]

theorem dilation.to_fun_eq_coe {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] {f : dilation α β} :

f.to_fun = ⇑f

@[simp]

theorem dilation.coe_mk {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : α → β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_edist.edist (f x) (f y) = ↑r * has_edist.edist x y) :

⇑{to_fun := f, edist_eq' := h} = f

theorem dilation.congr_fun {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] {f g : dilation α β} (h : f = g) (x : α) :

⇑f x = ⇑g x

theorem dilation.congr_arg {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) {x y : α} (h : x = y) :

⇑f x = ⇑f y

@[ext]

theorem dilation.ext {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] {f g : dilation α β} (h : ∀ (x : α), ⇑f x = ⇑g x) :

f = g

theorem dilation.ext_iff {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] {f g : dilation α β} :

f = g ↔ ∀ (x : α), ⇑f x = ⇑g x

@[simp]

theorem dilation.mk_coe {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_edist.edist (⇑f x) (⇑f y) = ↑r * has_edist.edist x y) :

{to_fun := ⇑f, edist_eq' := h} = f

@[simp]

theorem dilation.copy_to_fun {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) (f' : α → β) (h : f' = ⇑f) :

⇑(f.copy f' h) = f'

@[protected]

def dilation.copy {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) (f' : α → β) (h : f' = ⇑f) :

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

Equations

f.copy f' h = {to_fun := f', edist_eq' := _}

theorem dilation.copy_eq_self {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) {f' : α → β} (h : f' = ⇑f) :

f.copy f' h = f

noncomputable def dilation.ratio {α : Type u_1} {β : Type u_2} {F : Type u_4} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class 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

dilation.ratio f = ite (∀ (x y : α), has_edist.edist x y = 0 ∨ has_edist.edist x y = ⊤) 1 _.some

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

dilation.ratio f ≠ 0

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

0 < dilation.ratio f

@[simp]

theorem dilation.edist_eq {α : Type u_1} {β : Type u_2} {F : Type u_4} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) (x y : α) :

has_edist.edist (⇑f x) (⇑f y) = ↑(dilation.ratio f) * has_edist.edist x y

@[simp]

theorem dilation.nndist_eq {α : Type u_1} {β : Type u_2} {F : Type u_3} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) (x y : α) :

has_nndist.nndist (⇑f x) (⇑f y) = dilation.ratio f * has_nndist.nndist x y

@[simp]

theorem dilation.dist_eq {α : Type u_1} {β : Type u_2} {F : Type u_3} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) (x y : α) :

has_dist.dist (⇑f x) (⇑f y) = ↑(dilation.ratio f) * has_dist.dist x y

theorem dilation.ratio_unique {α : Type u_1} {β : Type u_2} {F : Type u_4} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] {f : F} {x y : α} {r : nnreal} (h₀ : has_edist.edist x y ≠ 0) (htop : has_edist.edist x y ≠ ⊤) (hr : has_edist.edist (⇑f x) (⇑f y) = ↑r * has_edist.edist x y) :

r = dilation.ratio f

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} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] {f : F} {x y : α} {r : nnreal} (hxy : has_nndist.nndist x y ≠ 0) (hr : has_nndist.nndist (⇑f x) (⇑f y) = r * has_nndist.nndist x y) :

r = dilation.ratio f

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} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] {f : F} {x y : α} {r : nnreal} (hxy : has_dist.dist x y ≠ 0) (hr : has_dist.dist (⇑f x) (⇑f y) = ↑r * has_dist.dist x y) :

r = dilation.ratio f

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} [pseudo_metric_space α] [pseudo_metric_space β] (f : α → β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_nndist.nndist (f x) (f y) = r * has_nndist.nndist x y) :

Alternative dilation constructor when the distance hypothesis is over nndist

Equations

dilation.mk_of_nndist_eq f h = {to_fun := f, edist_eq' := _}

@[simp]

theorem dilation.coe_mk_of_nndist_eq {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] (f : α → β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_nndist.nndist (f x) (f y) = r * has_nndist.nndist x y) :

⇑(dilation.mk_of_nndist_eq f h) = f

@[simp]

theorem dilation.mk_coe_of_nndist_eq {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] (f : dilation α β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_nndist.nndist (⇑f x) (⇑f y) = r * has_nndist.nndist x y) :

dilation.mk_of_nndist_eq ⇑f h = f

def dilation.mk_of_dist_eq {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] (f : α → β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_dist.dist (f x) (f y) = ↑r * has_dist.dist x y) :

Alternative dilation constructor when the distance hypothesis is over dist

Equations

dilation.mk_of_dist_eq f h = dilation.mk_of_nndist_eq f _

@[simp]

theorem dilation.coe_mk_of_dist_eq {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] (f : α → β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_dist.dist (f x) (f y) = ↑r * has_dist.dist x y) :

⇑(dilation.mk_of_dist_eq f h) = f

@[simp]

theorem dilation.mk_coe_of_dist_eq {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] (f : dilation α β) (h : ∃ (r : nnreal), r ≠ 0 ∧ ∀ (x y : α), has_dist.dist (⇑f x) (⇑f y) = ↑r * has_dist.dist x y) :

dilation.mk_of_dist_eq ⇑f h = f

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

lipschitz_with (dilation.ratio f) ⇑f

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

antilipschitz_with (dilation.ratio f)⁻¹ ⇑f

@[protected]

theorem dilation.injective {β : Type u_2} {F : Type u_4} [pseudo_emetric_space β] {α : Type u_1} [emetric_space α] [dilation_class F α β] (f : F) :

function.injective ⇑f

A dilation from an emetric space is injective

@[protected]

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

The identity is a dilation

Equations

dilation.id α = {to_fun := id α, edist_eq' := _}

@[protected, instance]

def dilation.inhabited {α : Type u_1} [pseudo_emetric_space α] :

inhabited (dilation α α)

Equations

dilation.inhabited = {default := dilation.id α _inst_1}

@[protected, simp]

theorem dilation.coe_id {α : Type u_1} [pseudo_emetric_space α] :

⇑(dilation.id α) = id

theorem dilation.id_ratio {α : Type u_1} [pseudo_emetric_space α] :

dilation.ratio (dilation.id α) = 1

def dilation.comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] (g : dilation β γ) (f : dilation α β) :

The composition of dilations is a dilation

Equations

g.comp f = {to_fun := ⇑g ∘ ⇑f, edist_eq' := _}

theorem dilation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {δ : Type u_4} [pseudo_emetric_space δ] (f : dilation α β) (g : dilation β γ) (h : dilation γ δ) :

(h.comp g).comp f = h.comp (g.comp f)

@[simp]

theorem dilation.coe_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] (g : dilation β γ) (f : dilation α β) :

⇑(g.comp f) = ⇑g ∘ ⇑f

theorem dilation.comp_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] (g : dilation β γ) (f : dilation α β) (x : α) :

⇑(g.comp f) x = ⇑g (⇑f x)

@[simp]

theorem dilation.comp_ratio {α : Type u_1} {β : Type u_2} {γ : Type u_3} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {g : dilation β γ} {f : dilation α β} (hne : ∃ (x y : α), has_edist.edist x y ≠ 0 ∧ has_edist.edist x y ≠ ⊤) :

dilation.ratio (g.comp f) = dilation.ratio g * dilation.ratio 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 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} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) :

f.comp (dilation.id α) = f

@[simp]

theorem dilation.id_comp {α : Type u_1} {β : Type u_2} [pseudo_emetric_space α] [pseudo_emetric_space β] (f : dilation α β) :

(dilation.id β).comp f = f

@[protected, instance]

def dilation.monoid {α : Type u_1} [pseudo_emetric_space α] :

monoid (dilation α α)

Equations

dilation.monoid = {mul := dilation.comp _inst_1, mul_assoc := _, one := dilation.id α _inst_1, one_mul := _, mul_one := _, npow := npow_rec (mul_one_class.to_has_mul (dilation α α)), npow_zero' := _, npow_succ' := _}

theorem dilation.one_def {α : Type u_1} [pseudo_emetric_space α] :

1 = dilation.id α

theorem dilation.mul_def {α : Type u_1} [pseudo_emetric_space α] (f g : dilation α α) :

f * g = f.comp g

@[simp]

theorem dilation.coe_one {α : Type u_1} [pseudo_emetric_space α] :

@[simp]

theorem dilation.coe_mul {α : Type u_1} [pseudo_emetric_space α] (f g : dilation α α) :

⇑(f * g) = ⇑f ∘ ⇑g

theorem dilation.cancel_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {g₁ g₂ : dilation β γ} {f : dilation α β} (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} [pseudo_emetric_space α] [pseudo_emetric_space β] [pseudo_emetric_space γ] {g : dilation β γ} {f₁ f₂ : dilation α β} (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} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) :

uniform_inducing ⇑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} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) {ι : Type u_3} {g : ι → α} {a : filter ι} {b : α} :

filter.tendsto g a (nhds b) ↔ filter.tendsto (⇑f ∘ g) a (nhds (⇑f b))

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

continuous ⇑f

A dilation is continuous.

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

emetric.diam (⇑f '' s) = ↑(dilation.ratio f) * emetric.diam 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} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) :

emetric.diam (set.range ⇑f) = ↑(dilation.ratio f) * emetric.diam set.univ

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} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) (x : α) (r : ennreal) :

set.maps_to ⇑f (emetric.ball x r) (emetric.ball (⇑f x) (↑(dilation.ratio f) * 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} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) (x : α) (r' : ennreal) :

set.maps_to ⇑f (emetric.closed_ball x r') (emetric.closed_ball (⇑f x) (↑(dilation.ratio f) * 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} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) {γ : Type u_3} [topological_space γ] {g : γ → α} {s : set γ} :

continuous_on (⇑f ∘ g) s ↔ continuous_on g s

theorem dilation.comp_continuous_iff {α : Type u_1} {β : Type u_2} {F : Type u_4} [pseudo_emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) {γ : Type u_3} [topological_space γ] {g : γ → α} :

continuous (⇑f ∘ g) ↔ continuous g

@[protected]

theorem dilation.uniform_embedding {α : Type u_1} {β : Type u_2} {F : Type u_4} [emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (f : F) :

uniform_embedding ⇑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} [emetric_space α] [pseudo_emetric_space β] [dilation_class F α β] (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} [emetric_space α] [complete_space α] [emetric_space β] [dilation_class F α β] (f : F) :

closed_embedding ⇑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} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) (s : set α) :

metric.diam (⇑f '' s) = ↑(dilation.ratio f) * metric.diam 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} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) :

metric.diam (set.range ⇑f) = ↑(dilation.ratio f) * metric.diam set.univ

theorem dilation.maps_to_ball {α : Type u_1} {β : Type u_2} {F : Type u_4} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) (x : α) (r' : ℝ) :

set.maps_to ⇑f (metric.ball x r') (metric.ball (⇑f x) (↑(dilation.ratio f) * 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} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) (x : α) (r' : ℝ) :

set.maps_to ⇑f (metric.sphere x r') (metric.sphere (⇑f x) (↑(dilation.ratio f) * 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} [pseudo_metric_space α] [pseudo_metric_space β] [dilation_class F α β] (f : F) (x : α) (r' : ℝ) :

set.maps_to ⇑f (metric.closed_ball x r') (metric.closed_ball (⇑f x) (↑(dilation.ratio f) * r'))

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