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 ofrin the relation above, defaulting to 1 in the case where it is not well-defined.
Notation #
α →ᵈ β: notation forDilation α β.
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
IsometryAPI to match the*HomClassAPI below.
References #
- https://en.wikipedia.org/wiki/Dilation_(metric_space)
- [Marcel Berger, Geometry][berger1987]
structure
Dilation
(α : Type u_1)
(β : Type u_2)
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
:
Type (max u_1 u_2)
A dilation is a map that uniformly scales the edistance between any two points.
- toFun : α → β
Equations
- «term_→ᵈ_» = Lean.ParserDescr.trailingNode `term_→ᵈ_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᵈ ") (Lean.ParserDescr.cat `term 26))
class
DilationClass
(F : Type u_3)
(α : Type u_4)
(β : Type u_5)
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
:
DilationClass F α β r states that F is a type of r-dilations.
You should extend this typeclass when you extend Dilation.
instance
Dilation.funLike
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
:
Equations
- Dilation.funLike = { coe := Dilation.toFun, coe_injective' := ⋯ }
instance
Dilation.toDilationClass
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
:
DilationClass (α →ᵈ β) α β
Equations
- ⋯ = ⋯
instance
Dilation.instCoeFunDilationForAll
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
:
Equations
- Dilation.instCoeFunDilationForAll = DFunLike.hasCoeToFun
@[simp]
theorem
Dilation.toFun_eq_coe
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{f : α →ᵈ β}
:
f.toFun = ⇑f
@[simp]
theorem
Dilation.coe_mk
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{f : α →ᵈ β}
{g : α →ᵈ β}
(h : f = g)
(x : α)
:
f x = g x
theorem
Dilation.congr_arg
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α →ᵈ β)
{x : α}
{y : α}
(h : x = y)
:
f x = f y
theorem
Dilation.ext
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{f : α →ᵈ β}
{g : α →ᵈ β}
(h : ∀ (x : α), f x = g x)
:
f = g
theorem
Dilation.ext_iff
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{f : α →ᵈ β}
{g : α →ᵈ β}
:
@[simp]
theorem
Dilation.mk_coe
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α →ᵈ β)
(f' : α → β)
(h : f' = ⇑f)
:
⇑(Dilation.copy f f' h) = f'
def
Dilation.copy
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α →ᵈ β)
(f' : α → β)
(h : f' = ⇑f)
:
α →ᵈ β
Copy of a Dilation with a new toFun equal to the old one. Useful to fix definitional
equalities.
Equations
- Dilation.copy f f' h = { toFun := f', edist_eq' := ⋯ }
theorem
Dilation.copy_eq_self
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α →ᵈ β)
{f' : α → β}
(h : f' = ⇑f)
:
Dilation.copy f f' h = f
def
Dilation.ratio
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass 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 = if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1 else Exists.choose ⋯
theorem
Dilation.ratio_of_trivial
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(h : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤)
:
Dilation.ratio f = 1
theorem
Dilation.ratio_of_subsingleton
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[Subsingleton α]
[DilationClass F α β]
(f : F)
:
Dilation.ratio f = 1
theorem
Dilation.ratio_ne_zero
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
Dilation.ratio f ≠ 0
theorem
Dilation.ratio_pos
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
0 < Dilation.ratio f
@[simp]
theorem
Dilation.edist_eq
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(y : α)
:
edist (f x) (f y) = ↑(Dilation.ratio f) * edist x y
@[simp]
theorem
Dilation.nndist_eq
{α : Type u_6}
{β : Type u_7}
{F : Type u_8}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(y : α)
:
nndist (f x) (f y) = Dilation.ratio f * nndist x y
@[simp]
theorem
Dilation.dist_eq
{α : Type u_6}
{β : Type u_7}
{F : Type u_8}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(y : α)
:
dist (f x) (f y) = ↑(Dilation.ratio f) * dist x y
theorem
Dilation.ratio_unique
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass 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)
:
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_6}
{β : Type u_7}
{F : Type u_8}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
{f : F}
{x : α}
{y : α}
{r : NNReal}
(hxy : nndist x y ≠ 0)
(hr : nndist (f x) (f y) = r * 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_7}
{β : Type u_8}
{F : Type u_6}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
{f : F}
{x : α}
{y : α}
{r : NNReal}
(hxy : dist x y ≠ 0)
(hr : dist (f x) (f y) = ↑r * 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.mkOfNNDistEq
{α : Type u_6}
{β : Type u_7}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
(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
- Dilation.mkOfNNDistEq f h = { toFun := f, edist_eq' := ⋯ }
@[simp]
theorem
Dilation.coe_mkOfNNDistEq
{α : Type u_6}
{β : Type u_7}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
(f : α → β)
(h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y)
:
⇑(Dilation.mkOfNNDistEq f h) = f
@[simp]
theorem
Dilation.mk_coe_of_nndist_eq
{α : Type u_6}
{β : Type u_7}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
(f : α →ᵈ β)
(h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), nndist (f x) (f y) = r * nndist x y)
:
Dilation.mkOfNNDistEq (⇑f) h = f
def
Dilation.mkOfDistEq
{α : Type u_6}
{β : Type u_7}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
(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
@[simp]
theorem
Dilation.coe_mkOfDistEq
{α : Type u_6}
{β : Type u_7}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
(f : α → β)
(h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y)
:
⇑(Dilation.mkOfDistEq f h) = f
@[simp]
theorem
Dilation.mk_coe_of_dist_eq
{α : Type u_6}
{β : Type u_7}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
(f : α →ᵈ β)
(h : ∃ (r : NNReal), r ≠ 0 ∧ ∀ (x y : α), dist (f x) (f y) = ↑r * dist x y)
:
Dilation.mkOfDistEq (⇑f) h = f
@[simp]
theorem
Isometry.toDilation_toFun
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α → β)
(hf : Isometry f)
:
∀ (a : α), (Isometry.toDilation f hf) a = f a
def
Isometry.toDilation
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α → β)
(hf : Isometry f)
:
α →ᵈ β
Every isometry is a dilation of ratio 1.
Equations
- Isometry.toDilation f hf = { toFun := f, edist_eq' := ⋯ }
@[simp]
theorem
Isometry.toDilation_ratio
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
{f : α → β}
{hf : Isometry f}
:
Dilation.ratio (Isometry.toDilation f hf) = 1
theorem
Dilation.lipschitz
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
LipschitzWith (Dilation.ratio f) ⇑f
theorem
Dilation.antilipschitz
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
theorem
Dilation.injective
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace β]
{α : Type u_6}
[EMetricSpace α]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
A dilation from an emetric space is injective
The identity is a dilation
Equations
- Dilation.id α = { toFun := id, edist_eq' := ⋯ }
Equations
- Dilation.instInhabitedDilation = { default := Dilation.id α }
def
Dilation.comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
(g : β →ᵈ γ)
(f : α →ᵈ β)
:
α →ᵈ γ
The composition of dilations is a dilation
Equations
- Dilation.comp g f = { toFun := ⇑g ∘ ⇑f, edist_eq' := ⋯ }
theorem
Dilation.comp_assoc
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
{δ : Type u_6}
[PseudoEMetricSpace δ]
(f : α →ᵈ β)
(g : β →ᵈ γ)
(h : γ →ᵈ δ)
:
Dilation.comp (Dilation.comp h g) f = Dilation.comp h (Dilation.comp g f)
@[simp]
theorem
Dilation.coe_comp
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
(g : β →ᵈ γ)
(f : α →ᵈ β)
:
⇑(Dilation.comp g f) = ⇑g ∘ ⇑f
theorem
Dilation.comp_apply
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
(g : β →ᵈ γ)
(f : α →ᵈ β)
(x : α)
:
(Dilation.comp g f) x = g (f x)
theorem
Dilation.ratio_comp'
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
{g : β →ᵈ γ}
{f : α →ᵈ β}
(hne : ∃ (x : α) (y : α), edist x y ≠ 0 ∧ edist x y ≠ ⊤)
:
Dilation.ratio (Dilation.comp g 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 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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α →ᵈ β)
:
Dilation.comp f (Dilation.id α) = f
@[simp]
theorem
Dilation.id_comp
{α : Type u_1}
{β : Type u_2}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
(f : α →ᵈ β)
:
Dilation.comp (Dilation.id β) f = f
theorem
Dilation.mul_def
{α : Type u_1}
[PseudoEMetricSpace α]
(f : α →ᵈ α)
(g : α →ᵈ α)
:
f * g = Dilation.comp f g
@[simp]
@[simp]
@[simp]
theorem
Dilation.ratio_mul
{α : Type u_1}
[PseudoEMetricSpace α]
(f : α →ᵈ α)
(g : α →ᵈ α)
:
Dilation.ratio (f * g) = Dilation.ratio f * Dilation.ratio g
@[simp]
theorem
Dilation.ratioHom_apply
{α : Type u_1}
[PseudoEMetricSpace α]
(f : α →ᵈ α)
:
Dilation.ratioHom f = Dilation.ratio f
Dilation.ratio as a monoid homomorphism from α →ᵈ α to ℝ≥0.
Equations
- Dilation.ratioHom = { toOneHom := { toFun := Dilation.ratio, map_one' := ⋯ }, map_mul' := ⋯ }
@[simp]
theorem
Dilation.ratio_pow
{α : Type u_1}
[PseudoEMetricSpace α]
(f : α →ᵈ α)
(n : ℕ)
:
Dilation.ratio (f ^ n) = Dilation.ratio f ^ n
@[simp]
theorem
Dilation.cancel_right
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
{g₁ : β →ᵈ γ}
{g₂ : β →ᵈ γ}
{f : α →ᵈ β}
(hf : Function.Surjective ⇑f)
:
Dilation.comp g₁ f = Dilation.comp g₂ f ↔ g₁ = g₂
@[simp]
theorem
Dilation.cancel_left
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
{g : β →ᵈ γ}
{f₁ : α →ᵈ β}
{f₂ : α →ᵈ β}
(hg : Function.Injective ⇑g)
:
Dilation.comp g f₁ = Dilation.comp g f₂ ↔ f₁ = f₂
theorem
Dilation.uniformInducing
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass 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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
{ι : Type u_6}
{g : ι → α}
{a : Filter ι}
{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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
Continuous ⇑f
A dilation is continuous.
theorem
Dilation.ediam_image
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass 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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass 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.mapsTo_emetric_ball
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(r : ENNReal)
:
Set.MapsTo (⇑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.mapsTo_emetric_closedBall
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(r' : ENNReal)
:
Set.MapsTo (⇑f) (EMetric.closedBall x r') (EMetric.closedBall (f x) (↑(Dilation.ratio f) * 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}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
{γ : Type u_6}
[TopologicalSpace γ]
{g : γ → α}
{s : Set γ}
:
ContinuousOn (⇑f ∘ g) s ↔ ContinuousOn g s
theorem
Dilation.comp_continuous_iff
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoEMetricSpace α]
[PseudoEMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
{γ : Type u_6}
[TopologicalSpace γ]
{g : γ → α}
:
Continuous (⇑f ∘ g) ↔ Continuous g
theorem
Dilation.uniformEmbedding
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[EMetricSpace α]
[FunLike F α β]
[PseudoEMetricSpace β]
[DilationClass 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}
[EMetricSpace α]
[FunLike F α β]
[PseudoEMetricSpace β]
[DilationClass F α β]
(f : F)
:
Embedding ⇑f
A dilation from a metric space is an embedding
theorem
Dilation.closedEmbedding
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[EMetricSpace α]
[FunLike F α β]
[CompleteSpace α]
[EMetricSpace β]
[DilationClass 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}
[MetricSpace α]
[Nontrivial α]
[PseudoEMetricSpace β]
[PseudoEMetricSpace γ]
{g : β →ᵈ γ}
{f : α →ᵈ β}
:
Dilation.ratio (Dilation.comp g 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 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}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass 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}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
Metric.diam (Set.range ⇑f) = ↑(Dilation.ratio f) * Metric.diam Set.univ
theorem
Dilation.mapsTo_ball
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(r' : ℝ)
:
Set.MapsTo (⇑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.mapsTo_sphere
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(r' : ℝ)
:
Set.MapsTo (⇑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.mapsTo_closedBall
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
(x : α)
(r' : ℝ)
:
Set.MapsTo (⇑f) (Metric.closedBall x r') (Metric.closedBall (f x) (↑(Dilation.ratio f) * 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}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
Filter.Tendsto (⇑f) (Bornology.cobounded α) (Bornology.cobounded β)
@[simp]
theorem
Dilation.comap_cobounded
{α : Type u_1}
{β : Type u_2}
{F : Type u_4}
[PseudoMetricSpace α]
[PseudoMetricSpace β]
[FunLike F α β]
[DilationClass F α β]
(f : F)
:
Filter.comap (⇑f) (Bornology.cobounded β) = Bornology.cobounded α