Mathlib.Topology.MetricSpace.Dilation

Dilation structure

Full source

/-- A dilation is a map that uniformly scales the edistance between any two points. -/
structure Dilation where
  toFun : α → β
  edist_eq' : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, edist (toFun x) (toFun y) = r * edist x y

Dilation between pseudo-emetric spaces

Informal description

A dilation between two pseudo-emetric spaces $\alpha$ and $\beta$ is a map $f \colon \alpha \to \beta$ that uniformly scales the extended distance between any two points, i.e., there exists a positive real number $r \notin \{0, \infty\}$ such that for all $x, y \in \alpha$, the extended distance satisfies $\text{edist}(f x, f y) = r \cdot \text{edist}(x, y)$. This ensures the map is injective and avoids infinite scaling factors.

term_→ᵈ_ definition

: Lean.TrailingParserDescr✝

Full source

@[inherit_doc] infixl:25 " →ᵈ " => Dilation

Dilation notation

Informal description

The notation `α →ᵈ β` represents the type of dilations from a pseudo-emetric space `α` to another pseudo-emetric space `β`. A dilation is a map `f : α → β` that satisfies the condition `edist (f x) (f y) = r * edist x y` for some positive real number `r` (i.e., `r ∉ {0, ∞}`). This ensures that the map is automatically injective and avoids infinite scaling factors.

DilationClass structure

(F : Type*) (α β : outParam Type*) [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β]

Full source

/-- `DilationClass F α β r` states that `F` is a type of `r`-dilations.
You should extend this typeclass when you extend `Dilation`. -/
class DilationClass (F : Type*) (α β : outParam Type*) [PseudoEMetricSpace α] [PseudoEMetricSpace β]
    [FunLike F α β] : Prop where
  edist_eq' : ∀ f : F, ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, edist (f x) (f y) = r * edist x y

Dilation Class

Informal description

The class `DilationClass F α β` states that `F` is a type of dilations between pseudo-extended metric spaces `α` and `β`, where each dilation `f : F` satisfies the condition that there exists a ratio `r ∈ ℝ≥0 \ {0, ∞}` such that for all `x, y ∈ α`, the extended distance between `f x` and `f y` is equal to `r` times the extended distance between `x` and `y`. This ensures that dilations are automatically injective and have a well-defined finite ratio.

Dilation.funLike instance

: FunLike (α →ᵈ β) α β

Full source

instance funLike : FunLike (α →ᵈ β) α β where
  coe := toFun
  coe_injective' f g h := by cases f; cases g; congr

Dilations as Function-Like Types

Informal description

For any two pseudo-emetric spaces $\alpha$ and $\beta$, the type of dilations $\alpha \toᵈ \beta$ can be treated as a function-like type, where each dilation $f \colon \alpha \toᵈ \beta$ can be coerced to a function from $\alpha$ to $\beta$.

Dilation.toDilationClass instance

: DilationClass (α →ᵈ β) α β

Full source

instance toDilationClass : DilationClass (α →ᵈ β) α β where
  edist_eq' f := edist_eq' f

Dilations Form a Dilation Class

Informal description

The type of dilations $\alpha \toᵈ \beta$ between pseudo-emetric spaces $\alpha$ and $\beta$ forms a dilation class, meaning every dilation $f \colon \alpha \toᵈ \beta$ satisfies the condition that there exists a ratio $r \in \mathbb{R}_{\ge 0} \setminus \{0, \infty\}$ such that for all $x, y \in \alpha$, the extended distance $\text{edist}(f x, f y) = r \cdot \text{edist}(x, y)$.

Dilation.toFun_eq_coe theorem

{f : α →ᵈ β} : f.toFun = (f : α → β)

Full source

@[simp]
theorem toFun_eq_coe {f : α →ᵈ β} : f.toFun = (f : α → β) :=
  rfl

Equality of Dilation's Underlying Function and its Coercion

Informal description

For any dilation $f \colon \alpha \toᵈ \beta$ between pseudo-emetric spaces, the underlying function $f.\text{toFun}$ is equal to the coercion of $f$ to a function from $\alpha$ to $\beta$.

Dilation.coe_mk theorem

(f : α → β) (h) : ⇑(⟨f, h⟩ : α →ᵈ β) = f

Full source

@[simp]
theorem coe_mk (f : α → β) (h) : ⇑(⟨f, h⟩ : α →ᵈ β) = f :=
  rfl

Coercion of Dilation Construction Equals Original Function

Informal description

For any function $f \colon \alpha \to \beta$ and proof $h$ that $f$ is a dilation, the coercion of the dilation structure $\langle f, h \rangle$ to a function is equal to $f$ itself.

Dilation.congr_fun theorem

{f g : α →ᵈ β} (h : f = g) (x : α) : f x = g x

Full source

protected theorem congr_fun {f g : α →ᵈ β} (h : f = g) (x : α) : f x = g x :=
  DFunLike.congr_fun h x

Pointwise Equality of Dilations

Informal description

For any two dilations $f, g \colon \alpha \toᵈ \beta$ between pseudo-emetric spaces, if $f = g$, then for all $x \in \alpha$, the evaluations $f(x)$ and $g(x)$ are equal.

Dilation.congr_arg theorem

(f : α →ᵈ β) {x y : α} (h : x = y) : f x = f y

Full source

protected theorem congr_arg (f : α →ᵈ β) {x y : α} (h : x = y) : f x = f y :=
  DFunLike.congr_arg f h

Dilation preserves equality

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-emetric spaces and any points $x, y \in \alpha$, if $x = y$, then $f(x) = f(y)$.

Dilation.ext theorem

{f g : α →ᵈ β} (h : ∀ x, f x = g x) : f = g

Full source

@[ext]
theorem ext {f g : α →ᵈ β} (h : ∀ x, f x = g x) : f = g :=
  DFunLike.ext f g h

Extensionality of Dilations

Informal description

For any two dilations $f, g \colon \alpha \toᵈ \beta$ between pseudo-emetric spaces, if $f(x) = g(x)$ for all $x \in \alpha$, then $f = g$.

Dilation.mk_coe theorem

(f : α →ᵈ β) (h) : Dilation.mk f h = f

Full source

@[simp]
theorem mk_coe (f : α →ᵈ β) (h) : Dilation.mk f h = f :=
  ext fun _ => rfl

Dilation Construction Equals Original Function

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-emetric spaces, the construction `Dilation.mk f h` is equal to $f$ itself, where `h` is a proof that $f$ satisfies the dilation property.

Dilation.copy definition

(f : α →ᵈ β) (f' : α → β) (h : f' = ⇑f) : α →ᵈ β

Full source

/-- Copy of a `Dilation` with a new `toFun` equal to the old one. Useful to fix definitional
equalities. -/
@[simps -fullyApplied]
protected def copy (f : α →ᵈ β) (f' : α → β) (h : f' = ⇑f) : α →ᵈ β where
  toFun := f'
  edist_eq' := h.symm ▸ f.edist_eq'

Copy of a dilation with a new function

Informal description

Given a dilation $f \colon \alpha \toᵈ \beta$ between pseudo-emetric spaces and a function $f' \colon \alpha \to \beta$ that is definitionally equal to $f$, the function `Dilation.copy` constructs a new dilation with the same scaling behavior as $f$ but using $f'$ as the underlying function. This is useful for fixing definitional equalities.

Dilation.copy_eq_self theorem

(f : α →ᵈ β) {f' : α → β} (h : f' = f) : f.copy f' h = f

Full source

theorem copy_eq_self (f : α →ᵈ β) {f' : α → β} (h : f' = f) : f.copy f' h = f :=
  DFunLike.ext' h

Copy of a Dilation with Identical Function Yields Original Dilation

Informal description

For any dilation $f \colon \alpha \toᵈ \beta$ between pseudo-emetric spaces and any function $f' \colon \alpha \to \beta$ such that $f' = f$, the copy of $f$ with $f'$ as the underlying function is equal to $f$ itself.

Dilation.ratio definition

[DilationClass F α β] (f : F) : ℝ≥0

Full source

/-- 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. -/
def ratio [DilationClass F α β] (f : F) : ℝ≥0 :=
  if ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤ then 1 else (DilationClass.edist_eq' f).choose

Ratio of a dilation

Informal description

For a dilation $ f $ between pseudo-extended metric spaces $ \alpha $ and $ \beta $, the ratio $ \text{ratio}(f) \in \mathbb{R}_{\geq 0} $ is defined as the unique positive real number $ r $ such that for all $ x, y \in \alpha $, the extended distance satisfies $ \text{edist}(f x, f y) = r \cdot \text{edist}(x, y) $. If no such $ r $ exists (i.e., all distances in $ \alpha $ are either zero or infinity), the ratio defaults to 1.

Dilation.ratio_of_trivial theorem

[DilationClass F α β] (f : F) (h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞) : ratio f = 1

Full source

theorem ratio_of_trivial [DilationClass F α β] (f : F)
    (h : ∀ x y : α, edistedist x y = 0 ∨ edist x y = ∞) : ratio f = 1 :=
  if_pos h

Dilation Ratio is One for Trivial Spaces

Informal description

For any dilation $f$ between pseudo-extended metric spaces $\alpha$ and $\beta$, if for all $x, y \in \alpha$ the extended distance $\text{edist}(x, y)$ is either $0$ or $\infty$, then the ratio of $f$ is equal to $1$.

Dilation.ratio_of_subsingleton theorem

[Subsingleton α] [DilationClass F α β] (f : F) : ratio f = 1

Full source

@[nontriviality]
theorem ratio_of_subsingleton [Subsingleton α] [DilationClass F α β] (f : F) : ratio f = 1 :=
  if_pos fun x y ↦ by simp [Subsingleton.elim x y]

Dilation ratio is 1 for subsingleton domain

Informal description

For any dilation $f$ between pseudo-extended metric spaces $\alpha$ and $\beta$, if $\alpha$ is a subsingleton (i.e., all elements of $\alpha$ are equal), then the ratio of $f$ is equal to $1$.

Dilation.ratio_ne_zero theorem

[DilationClass F α β] (f : F) : ratio f ≠ 0

Full source

theorem ratio_ne_zero [DilationClass F α β] (f : F) : ratioratio f ≠ 0 := by
  rw [ratio]; split_ifs
  · exact one_ne_zero
  exact (DilationClass.edist_eq' f).choose_spec.1

Nonzero Ratio Property of Dilations

Informal description

For any dilation $f$ between pseudo-extended metric spaces $\alpha$ and $\beta$, the ratio $\text{ratio}(f) \in \mathbb{R}_{\geq 0}$ is nonzero.

Dilation.ratio_pos theorem

[DilationClass F α β] (f : F) : 0 < ratio f

Full source

theorem ratio_pos [DilationClass F α β] (f : F) : 0 < ratio f :=
  (ratio_ne_zero f).bot_lt

Positivity of Dilation Ratio

Informal description

For any dilation $f$ between pseudo-extended metric spaces $\alpha$ and $\beta$, the ratio $\text{ratio}(f)$ is strictly positive, i.e., $0 < \text{ratio}(f)$.

Dilation.edist_eq theorem

[DilationClass F α β] (f : F) (x y : α) : edist (f x) (f y) = ratio f * edist x y

Full source

@[simp]
theorem edist_eq [DilationClass F α β] (f : F) (x y : α) :
    edist (f x) (f y) = ratio f * edist x y := by
  rw [ratio]; split_ifs with key
  · rcases DilationClass.edist_eq' f with ⟨r, hne, hr⟩
    replace hr := hr x y
    rcases key x y with h | h
    · simp only [hr, h, mul_zero]
    · simp [hr, h, hne]
  exact (DilationClass.edist_eq' f).choose_spec.2 x y

Dilation Property: $\text{edist}(f(x), f(y)) = r \cdot \text{edist}(x, y)$

Informal description

For any dilation $f$ between pseudo-extended metric spaces $\alpha$ and $\beta$, and for any two points $x, y \in \alpha$, the extended distance between $f(x)$ and $f(y)$ is equal to the ratio of $f$ multiplied by the extended distance between $x$ and $y$, i.e., \[ \text{edist}(f(x), f(y)) = r \cdot \text{edist}(x, y), \] where $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0} \setminus \{0, \infty\}$ is the dilation ratio of $f$.

Dilation.nndist_eq theorem

 {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x y : α) :
  nndist (f x) (f y) = ratio f * nndist x y

Full source

@[simp]
theorem nndist_eq {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β]
    [DilationClass F α β] (f : F) (x y : α) :
    nndist (f x) (f y) = ratio f * nndist x y := by
  simp only [← ENNReal.coe_inj, ← edist_nndist, ENNReal.coe_mul, edist_eq]

Dilation Property for Non-Negative Distance: $\text{nndist}(f(x), f(y)) = r \cdot \text{nndist}(x, y)$

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation between them. For any two points $x, y \in \alpha$, the non-negative distance between $f(x)$ and $f(y)$ is equal to the ratio of $f$ multiplied by the non-negative distance between $x$ and $y$, i.e., \[ \text{nndist}(f(x), f(y)) = r \cdot \text{nndist}(x, y), \] where $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0}$ is the dilation ratio of $f$.

Dilation.dist_eq theorem

 {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) (x y : α) :
  dist (f x) (f y) = ratio f * dist x y

Full source

@[simp]
theorem dist_eq {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β]
    [DilationClass F α β] (f : F) (x y : α) :
    dist (f x) (f y) = ratio f * dist x y := by
  simp only [dist_nndist, nndist_eq, NNReal.coe_mul]

Dilation Property: $\text{dist}(f(x), f(y)) = r \cdot \text{dist}(x, y)$

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation between them. For any two points $x, y \in \alpha$, the distance between $f(x)$ and $f(y)$ is equal to the ratio of $f$ multiplied by the distance between $x$ and $y$, i.e., \[ \text{dist}(f(x), f(y)) = r \cdot \text{dist}(x, y), \] where $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0}$ is the dilation ratio of $f$.

Dilation.ratio_unique theorem

 [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (h₀ : edist x y ≠ 0) (htop : edist x y ≠ ⊤)
  (hr : edist (f x) (f y) = r * edist x y) : r = ratio f

Full source

/-- The `ratio` is equal to the distance ratio for any two points with nonzero finite distance.
`dist` and `nndist` versions below -/
theorem ratio_unique [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (h₀ : edistedist x y ≠ 0)
    (htop : edistedist x y ≠ ⊤) (hr : edist (f x) (f y) = r * edist x y) : r = ratio f := by
  simpa only [hr, ENNReal.mul_left_inj h₀ htop, ENNReal.coe_inj] using edist_eq f x y

Uniqueness of Dilation Ratio for Nonzero Finite Distances

Informal description

Let $f : \alpha \to \beta$ be a dilation between pseudo-extended metric spaces $\alpha$ and $\beta$, and let $x, y \in \alpha$ be points such that the extended distance $\text{edist}(x, y)$ is neither zero nor infinity. If there exists a nonnegative real number $r \in \mathbb{R}_{\geq 0}$ such that $\text{edist}(f(x), f(y)) = r \cdot \text{edist}(x, y)$, then $r$ must be equal to the dilation ratio of $f$, i.e., $r = \text{ratio}(f)$.

Dilation.ratio_unique_of_nndist_ne_zero theorem

 {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] {f : F} {x y : α}
  {r : ℝ≥0} (hxy : nndist x y ≠ 0) (hr : nndist (f x) (f y) = r * nndist x y) : r = ratio f

Full source

/-- The `ratio` is equal to the distance ratio for any two points
with nonzero finite distance; `nndist` version -/
theorem ratio_unique_of_nndist_ne_zero {α β F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β]
    [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : nndistnndist x y ≠ 0)
    (hr : nndist (f x) (f y) = r * nndist x y) : r = ratio f :=
  ratio_unique (by rwa [edist_nndist, ENNReal.coe_ne_zero]) (edist_ne_top x y)
    (by rw [edist_nndist, edist_nndist, hr, ENNReal.coe_mul])

Uniqueness of Dilation Ratio for Nonzero Non-Negative Distances

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation. For any two points $x, y \in \alpha$ with nonzero non-negative distance ($\text{nndist}(x, y) \neq 0$), if there exists a nonnegative real number $r \in \mathbb{R}_{\geq 0}$ such that $\text{nndist}(f(x), f(y)) = r \cdot \text{nndist}(x, y)$, then $r$ must be equal to the dilation ratio of $f$, i.e., $r = \text{ratio}(f)$.

Dilation.ratio_unique_of_dist_ne_zero theorem

 {α β} {F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] {f : F} {x y : α}
  {r : ℝ≥0} (hxy : dist x y ≠ 0) (hr : dist (f x) (f y) = r * dist x y) : r = ratio f

Full source

/-- The `ratio` is equal to the distance ratio for any two points
with nonzero finite distance; `dist` version -/
theorem ratio_unique_of_dist_ne_zero {α β} {F : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β]
    [FunLike F α β] [DilationClass F α β] {f : F} {x y : α} {r : ℝ≥0} (hxy : distdist x y ≠ 0)
    (hr : dist (f x) (f y) = r * dist x y) : r = ratio f :=
  ratio_unique_of_nndist_ne_zero (NNReal.coe_ne_zero.1 hxy) <|
    NNReal.eq <| by rw [coe_nndist, hr, NNReal.coe_mul, coe_nndist]

Uniqueness of Dilation Ratio for Nonzero Distances

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation. For any two points $x, y \in \alpha$ with nonzero distance ($\text{dist}(x, y) \neq 0$), if there exists a nonnegative real number $r \in \mathbb{R}_{\geq 0}$ such that $\text{dist}(f(x), f(y)) = r \cdot \text{dist}(x, y)$, then $r$ must be equal to the dilation ratio of $f$, i.e., $r = \text{ratio}(f)$.

Dilation.mkOfNNDistEq definition

 {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
  (h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, nndist (f x) (f y) = r * nndist x y) : α →ᵈ β

Full source

/-- Alternative `Dilation` constructor when the distance hypothesis is over `nndist` -/
def mkOfNNDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
    (h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, nndist (f x) (f y) = r * nndist x y) : α →ᵈ β where
  toFun := f
  edist_eq' := by
    rcases h with ⟨r, hne, h⟩
    refine ⟨r, hne, fun x y => ?_⟩
    rw [edist_nndist, edist_nndist, ← ENNReal.coe_mul, h x y]

Dilation constructor from non-negative distance condition

Informal description

Given a function $ f \colon \alpha \to \beta $ between pseudometric spaces $\alpha$ and $\beta$, if there exists a positive real number $ r \neq 0 $ such that for all $ x, y \in \alpha $, the non-negative distance satisfies $ \text{nndist}(f x, f y) = r \cdot \text{nndist}(x, y) $, then $ f $ can be promoted to a dilation between $\alpha$ and $\beta$.

Dilation.coe_mkOfNNDistEq theorem

{α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h) : ⇑(mkOfNNDistEq f h : α →ᵈ β) = f

Full source

@[simp]
theorem coe_mkOfNNDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h) :
    ⇑(mkOfNNDistEq f h : α →ᵈ β) = f :=
  rfl

Coercion of Dilation Constructor Preserves Underlying Function

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \to \beta$ be a function. If there exists a positive real number $r \neq 0$ such that for all $x, y \in \alpha$, the non-negative distance satisfies $\text{nndist}(f x, f y) = r \cdot \text{nndist}(x, y)$, then the underlying function of the dilation constructed from $f$ and this condition is equal to $f$ itself. In other words, the coercion of $\text{mkOfNNDistEq}\,f\,h$ to a function coincides with $f$.

Dilation.mk_coe_of_nndist_eq theorem

{α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h) : Dilation.mkOfNNDistEq f h = f

Full source

@[simp]
theorem mk_coe_of_nndist_eq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β)
    (h) : Dilation.mkOfNNDistEq f h = f :=
  ext fun _ => rfl

Dilation Construction from Non-Negative Distance Property Yields Original Dilation

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \toᵈ \beta$ be a dilation. Then the construction of $f$ via `Dilation.mkOfNNDistEq` applied to $f$ and its scaling property $h$ yields $f$ itself, i.e., $\text{Dilation.mkOfNNDistEq}\,f\,h = f$.

Dilation.mkOfDistEq definition

 {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
  (h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, dist (f x) (f y) = r * dist x y) : α →ᵈ β

Full source

/-- Alternative `Dilation` constructor when the distance hypothesis is over `dist` -/
def mkOfDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β)
    (h : ∃ r : ℝ≥0, r ≠ 0 ∧ ∀ x y : α, dist (f x) (f y) = r * dist x y) : α →ᵈ β :=
  mkOfNNDistEq f <|
    h.imp fun r hr =>
      ⟨hr.1, fun x y => NNReal.eq <| by rw [coe_nndist, hr.2, NNReal.coe_mul, coe_nndist]⟩

Dilation constructor from distance condition

Informal description

Given a function $ f \colon \alpha \to \beta $ between pseudometric spaces $\alpha$ and $\beta$, if there exists a positive real number $ r \neq 0 $ such that for all $ x, y \in \alpha $, the distance satisfies $ \text{dist}(f x, f y) = r \cdot \text{dist}(x, y) $, then $ f $ can be promoted to a dilation between $\alpha$ and $\beta$.

Dilation.coe_mkOfDistEq theorem

{α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h) : ⇑(mkOfDistEq f h : α →ᵈ β) = f

Full source

@[simp]
theorem coe_mkOfDistEq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α → β) (h) :
    ⇑(mkOfDistEq f h : α →ᵈ β) = f :=
  rfl

Coercion of Dilation Constructed from Distance Condition Equals Original Function

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \to \beta$ be a function such that there exists a positive real number $r \neq 0$ with $\text{dist}(f x, f y) = r \cdot \text{dist}(x, y)$ for all $x, y \in \alpha$. Then the coercion of the dilation $\text{mkOfDistEq}\,f\,h \colon \alpha \toᵈ \beta$ is equal to $f$.

Dilation.mk_coe_of_dist_eq theorem

{α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h) : Dilation.mkOfDistEq f h = f

Full source

@[simp]
theorem mk_coe_of_dist_eq {α β} [PseudoMetricSpace α] [PseudoMetricSpace β] (f : α →ᵈ β) (h) :
    Dilation.mkOfDistEq f h = f :=
  ext fun _ => rfl

Dilation Construction from Distance Condition Yields Original Dilation

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \toᵈ \beta$ be a dilation. If there exists a positive real number $r \neq 0$ such that for all $x, y \in \alpha$, the distance satisfies $\text{dist}(f x, f y) = r \cdot \text{dist}(x, y)$, then the dilation constructed from this condition via `mkOfDistEq` is equal to $f$ itself.

Isometry.toDilation definition

(f : α → β) (hf : Isometry f) : α →ᵈ β

Full source

/-- Every isometry is a dilation of ratio `1`. -/
@[simps]
def _root_.Isometry.toDilation (f : α → β) (hf : Isometry f) : α →ᵈ β where
  toFun := f
  edist_eq' := ⟨1, one_ne_zero, by simpa using hf⟩

Dilation from an isometry with ratio 1

Informal description

Given an isometry $ f $ between two pseudo-emetric spaces $ \alpha $ and $ \beta $, the function `Isometry.toDilation` constructs a dilation from $ f $ with scaling ratio $ 1 $. This dilation satisfies the property that the extended distance between any two points $ x $ and $ y $ in $ \alpha $ is preserved under $ f $, i.e., $ \text{edist}(f x, f y) = 1 \cdot \text{edist}(x, y) $.

Isometry.toDilation_ratio theorem

{f : α → β} {hf : Isometry f} : ratio hf.toDilation = 1

Full source

@[simp]
lemma _root_.Isometry.toDilation_ratio {f : α → β} {hf : Isometry f} : ratio hf.toDilation = 1 := by
  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ⊤
  · exact ratio_of_trivial hf.toDilation h
  · push_neg at h
    obtain ⟨x, y, h₁, h₂⟩ := h
    exact ratio_unique h₁ h₂ (by simp [hf x y]) |>.symm

Dilation Ratio of Induced Isometry is One

Informal description

For any isometry $f \colon \alpha \to \beta$ between pseudo-emetric spaces, the dilation ratio of the induced dilation $hf.toDilation$ is equal to $1$.

Dilation.lipschitz theorem

: LipschitzWith (ratio f) (f : α → β)

Full source

theorem lipschitz : LipschitzWith (ratio f) (f : α → β) := fun x y => (edist_eq f x y).le

Lipschitz Property of Dilations: $\text{Lip}(f) = \text{ratio}(f)$

Informal description

For any dilation $f$ between pseudo-extended metric spaces $\alpha$ and $\beta$, the function $f$ is Lipschitz continuous with Lipschitz constant equal to the dilation ratio $\text{ratio}(f) \in \mathbb{R}_{\geq 0} \setminus \{0, \infty\}$. That is, for all $x, y \in \alpha$, we have \[ \text{edist}(f(x), f(y)) \leq \text{ratio}(f) \cdot \text{edist}(x, y). \]

Dilation.antilipschitz theorem

: AntilipschitzWith (ratio f)⁻¹ (f : α → β)

Full source

theorem antilipschitz : AntilipschitzWith (ratio f)⁻¹ (f : α → β) := fun x y => by
  have hr : ratioratio f ≠ 0 := ratio_ne_zero f
  exact mod_cast
    (ENNReal.mul_le_iff_le_inv (ENNReal.coe_ne_zero.2 hr) ENNReal.coe_ne_top).1 (edist_eq f x y).ge

Dilation is Antilipschitz with Inverse Ratio

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-extended metric spaces, the function $f$ is antilipschitz with constant $(\text{ratio}(f))^{-1}$, where $\text{ratio}(f) \in \mathbb{R}_{\geq 0} \setminus \{0, \infty\}$ is the dilation ratio of $f$. That is, for all $x, y \in \alpha$, the extended distance satisfies \[ \text{edist}(x, y) \leq (\text{ratio}(f))^{-1} \cdot \text{edist}(f(x), f(y)). \]

Dilation.injective theorem

{α : Type*} [EMetricSpace α] [FunLike F α β] [DilationClass F α β] (f : F) : Injective f

Full source

/-- A dilation from an emetric space is injective -/
protected theorem injective {α : Type*} [EMetricSpace α] [FunLike F α β] [DilationClass F α β]
    (f : F) :
    Injective f :=
  (antilipschitz f).injective

Injectivity of Dilations in Extended Metric Spaces

Informal description

Let $\alpha$ and $\beta$ be extended metric spaces, and let $F$ be a type of dilations between them. For any dilation $f \colon \alpha \to \beta$ with a finite nonzero ratio, $f$ is injective. That is, for any $x, y \in \alpha$, if $f(x) = f(y)$, then $x = y$.

Dilation.id definition

(α) [PseudoEMetricSpace α] : α →ᵈ α

Full source

/-- The identity is a dilation -/
protected def id (α) [PseudoEMetricSpace α] : α →ᵈ α where
  toFun := id
  edist_eq' := ⟨1, one_ne_zero, fun x y => by simp only [id, ENNReal.coe_one, one_mul]⟩

Identity dilation

Informal description

The identity map on a pseudo-emetric space $\alpha$ is a dilation with scaling ratio $1$. That is, for any $x, y \in \alpha$, the extended distance satisfies $\text{edist}(x, y) = 1 \cdot \text{edist}(x, y)$.

Dilation.instInhabited instance

: Inhabited (α →ᵈ α)

Full source

instance : Inhabited (α →ᵈ α) :=
  ⟨Dilation.id α⟩

Inhabited Type of Dilations on a Pseudo-EMetric Space

Informal description

For any pseudo-emetric space $\alpha$, the type of dilations $\alpha \to \alpha$ is inhabited, with the identity map as a canonical element.

Dilation.coe_id theorem

: ⇑(Dilation.id α) = id

Full source

@[simp]
protected theorem coe_id : ⇑(Dilation.id α) = id :=
  rfl

Identity Dilation Coerces to Identity Function

Informal description

The coercion of the identity dilation on a pseudo-emetric space $\alpha$ to a function is equal to the identity function on $\alpha$, i.e., $\text{id}_\alpha = \text{id}$.

Dilation.ratio_id theorem

: ratio (Dilation.id α) = 1

Full source

theorem ratio_id : ratio (Dilation.id α) = 1 := by
  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
  · rw [ratio, if_pos h]
  · push_neg at h
    rcases h with ⟨x, y, hne⟩
    refine (ratio_unique hne.1 hne.2 ?_).symm
    simp

Identity Dilation Has Ratio One

Informal description

For any pseudo-emetric space $\alpha$, the ratio of the identity dilation $\text{id}_\alpha \colon \alpha \to \alpha$ is equal to $1$.

Dilation.comp definition

(g : β →ᵈ γ) (f : α →ᵈ β) : α →ᵈ γ

Full source

/-- The composition of dilations is a dilation -/
def comp (g : β →ᵈ γ) (f : α →ᵈ β) : α →ᵈ γ where
  toFun := g ∘ f
  edist_eq' := ⟨ratio g * ratio f, mul_ne_zero (ratio_ne_zero g) (ratio_ne_zero f),
    fun x y => by simp_rw [Function.comp, edist_eq, ENNReal.coe_mul, mul_assoc]⟩

Composition of dilations

Informal description

The composition of two dilations $ g \colon \beta \to \gamma $ and $ f \colon \alpha \to \beta $ is a dilation $ g \circ f \colon \alpha \to \gamma $ whose scaling ratio is the product of the scaling ratios of $ g $ and $ f $. Specifically, for any $ x, y \in \alpha $, the extended distance satisfies $ \text{edist}((g \circ f)(x), (g \circ f)(y)) = r_g \cdot r_f \cdot \text{edist}(x, y) $, where $ r_g $ and $ r_f $ are the scaling ratios of $ g $ and $ f $ respectively.

Dilation.comp_assoc theorem

 {δ : Type*} [PseudoEMetricSpace δ] (f : α →ᵈ β) (g : β →ᵈ γ) (h : γ →ᵈ δ) : (h.comp g).comp f = h.comp (g.comp f)

Full source

theorem comp_assoc {δ : Type*} [PseudoEMetricSpace δ] (f : α →ᵈ β) (g : β →ᵈ γ)
    (h : γ →ᵈ δ) : (h.comp g).comp f = h.comp (g.comp f) :=
  rfl

Associativity of Dilation Composition

Informal description

For any pseudo-emetric spaces $\alpha$, $\beta$, $\gamma$, and $\delta$, and any dilations $f \colon \alpha \to \beta$, $g \colon \beta \to \gamma$, and $h \colon \gamma \to \delta$, the composition of dilations is associative. That is, $(h \circ g) \circ f = h \circ (g \circ f)$.

Dilation.coe_comp theorem

(g : β →ᵈ γ) (f : α →ᵈ β) : (g.comp f : α → γ) = g ∘ f

Full source

@[simp]
theorem coe_comp (g : β →ᵈ γ) (f : α →ᵈ β) : (g.comp f : α → γ) = g ∘ f :=
  rfl

Composition of Dilations as Function Composition

Informal description

For any dilations $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$ between pseudo-emetric spaces, the underlying function of their composition $g \circ f \colon \alpha \to \gamma$ is equal to the pointwise composition $g \circ f$ of the underlying functions.

Dilation.comp_apply theorem

(g : β →ᵈ γ) (f : α →ᵈ β) (x : α) : (g.comp f : α → γ) x = g (f x)

Full source

theorem comp_apply (g : β →ᵈ γ) (f : α →ᵈ β) (x : α) : (g.comp f : α → γ) x = g (f x) :=
  rfl

Evaluation of Composition of Dilations

Informal description

For any dilations $g \colon \beta \to \gamma$ and $f \colon \alpha \to \beta$ between pseudo-emetric spaces, and for any point $x \in \alpha$, the evaluation of the composition $g \circ f$ at $x$ is equal to $g$ evaluated at $f(x)$, i.e., $(g \circ f)(x) = g(f(x))$.

Dilation.ratio_comp' theorem

 {g : β →ᵈ γ} {f : α →ᵈ β} (hne : ∃ x y : α, edist x y ≠ 0 ∧ edist x y ≠ ⊤) : ratio (g.comp f) = ratio g * ratio f

Full source

/-- 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. -/
theorem ratio_comp' {g : β →ᵈ γ} {f : α →ᵈ β}
    (hne : ∃ x y : α, edist x y ≠ 0 ∧ edist x y ≠ ⊤) : ratio (g.comp f) = ratio g * ratio f := by
  rcases hne with ⟨x, y, hα⟩
  have hgf := (edist_eq (g.comp f) x y).symm
  simp_rw [coe_comp, Function.comp, edist_eq, ← mul_assoc, ENNReal.mul_left_inj hα.1 hα.2]
    at hgf
  rwa [← ENNReal.coe_inj, ENNReal.coe_mul]

Ratio of Composition of Dilations is Product of Ratios

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be dilations between pseudo-emetric spaces. If there exist points $x, y \in \alpha$ such that the extended distance $\text{edist}(x, y)$ is neither $0$ nor $\infty$, then the ratio of the composition $g \circ f$ is the product of their ratios, i.e., \[ \text{ratio}(g \circ f) = \text{ratio}(g) \cdot \text{ratio}(f). \]

Dilation.comp_id theorem

(f : α →ᵈ β) : f.comp (Dilation.id α) = f

Full source

@[simp]
theorem comp_id (f : α →ᵈ β) : f.comp (Dilation.id α) = f :=
  ext fun _ => rfl

Right Identity Law for Dilation Composition

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-emetric spaces, the composition of $f$ with the identity dilation on $\alpha$ is equal to $f$ itself, i.e., $f \circ \text{id}_\alpha = f$.

Dilation.id_comp theorem

(f : α →ᵈ β) : (Dilation.id β).comp f = f

Full source

@[simp]
theorem id_comp (f : α →ᵈ β) : (Dilation.id β).comp f = f :=
  ext fun _ => rfl

Identity Dilation Acts as Left Identity under Composition

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-emetric spaces, the composition of the identity dilation on $\beta$ with $f$ is equal to $f$, i.e., $\text{id}_\beta \circ f = f$.

Dilation.instMonoid instance

: Monoid (α →ᵈ α)

Full source

instance : Monoid (α →ᵈ α) where
  one := Dilation.id α
  mul := comp
  mul_one := comp_id
  one_mul := id_comp
  mul_assoc _ _ _ := comp_assoc _ _ _

Monoid Structure on Dilations of a Pseudo-EMetric Space

Informal description

For any pseudo-emetric space $\alpha$, the set of dilations from $\alpha$ to itself forms a monoid under composition, with the identity dilation as the neutral element.

Dilation.one_def theorem

: (1 : α →ᵈ α) = Dilation.id α

Full source

theorem one_def : (1 : α →ᵈ α) = Dilation.id α :=
  rfl

Identity Dilation as Monoid Unit

Informal description

The dilation corresponding to the multiplicative identity in the monoid of dilations on a pseudo-emetric space $\alpha$ is equal to the identity dilation, i.e., $1 = \text{id}_\alpha$.

Dilation.mul_def theorem

(f g : α →ᵈ α) : f * g = f.comp g

Full source

theorem mul_def (f g : α →ᵈ α) : f * g = f.comp g :=
  rfl

Product of Dilations Equals Composition

Informal description

For any two dilations $f$ and $g$ from a pseudo-emetric space $\alpha$ to itself, the product $f * g$ is equal to the composition $f \circ g$.

Dilation.coe_one theorem

: ⇑(1 : α →ᵈ α) = id

Full source

@[simp]
theorem coe_one : ⇑(1 : α →ᵈ α) = id :=
  rfl

Identity Dilation is the Identity Function

Informal description

The dilation corresponding to the multiplicative identity $1$ in the monoid of dilations from a pseudo-emetric space $\alpha$ to itself is equal to the identity function $\text{id} \colon \alpha \to \alpha$.

Dilation.coe_mul theorem

(f g : α →ᵈ α) : ⇑(f * g) = f ∘ g

Full source

@[simp]
theorem coe_mul (f g : α →ᵈ α) : ⇑(f * g) = f ∘ g :=
  rfl

Composition of Dilations as Function Composition

Informal description

For any two dilations $f, g \colon \alpha \toᵈ \alpha$ on a pseudo-emetric space $\alpha$, the underlying function of their composition $f * g$ is equal to the function composition $f \circ g$.

Dilation.ratio_one theorem

: ratio (1 : α →ᵈ α) = 1

Full source

@[simp] theorem ratio_one : ratio (1 : α →ᵈ α) = 1 := ratio_id

Identity Dilation Has Ratio One

Informal description

For any pseudo-emetric space $\alpha$, the ratio of the identity dilation $1 \colon \alpha \toᵈ \alpha$ is equal to $1$.

Dilation.ratio_mul theorem

(f g : α →ᵈ α) : ratio (f * g) = ratio f * ratio g

Full source

@[simp]
theorem ratio_mul (f g : α →ᵈ α) : ratio (f * g) = ratio f * ratio g := by
  by_cases h : ∀ x y : α, edist x y = 0 ∨ edist x y = ∞
  · simp [ratio_of_trivial, h]
  push_neg at h
  exact ratio_comp' h

Ratio of Composition of Dilations is Product of Ratios

Informal description

For any two dilations $f$ and $g$ from a pseudo-emetric space $\alpha$ to itself, the ratio of their composition $f \circ g$ is equal to the product of their individual ratios, i.e., \[ \text{ratio}(f \circ g) = \text{ratio}(f) \cdot \text{ratio}(g). \]

Dilation.ratioHom definition

: (α →ᵈ α) →* ℝ≥0

Full source

/-- `Dilation.ratio` as a monoid homomorphism from `α →ᵈ α` to `ℝ≥0`. -/
@[simps]
def ratioHom : (α →ᵈ α) →* ℝ≥0 := ⟨⟨ratio, ratio_one⟩, ratio_mul⟩

Ratio homomorphism for dilations

Informal description

The monoid homomorphism that maps each dilation $ f \colon \alpha \toᵈ \alpha $ to its ratio $ \text{ratio}(f) \in \mathbb{R}_{\geq 0} $, where $ \text{ratio}(f) $ is the unique positive real number $ r $ such that for all $ x, y \in \alpha $, the extended distance satisfies $ \text{edist}(f x, f y) = r \cdot \text{edist}(x, y) $. This homomorphism preserves the monoid structure, meaning it maps the identity dilation to 1 and the composition of dilations to the product of their ratios.

Dilation.ratio_pow theorem

(f : α →ᵈ α) (n : ℕ) : ratio (f ^ n) = ratio f ^ n

Full source

@[simp]
theorem ratio_pow (f : α →ᵈ α) (n : ℕ) : ratio (f ^ n) = ratio f ^ n :=
  ratioHom.map_pow _ _

Ratio of Iterated Dilation is Power of Ratio: $\text{ratio}(f^n) = \text{ratio}(f)^n$

Informal description

For any dilation $f \colon \alpha \to \alpha$ on a pseudo-emetric space $\alpha$ and any natural number $n$, the ratio of the $n$-th iterate of $f$ is equal to the $n$-th power of the ratio of $f$, i.e., \[ \text{ratio}(f^n) = (\text{ratio}(f))^n. \]

Dilation.cancel_right theorem

{g₁ g₂ : β →ᵈ γ} {f : α →ᵈ β} (hf : Surjective f) : g₁.comp f = g₂.comp f ↔ g₁ = g₂

Full source

@[simp]
theorem cancel_right {g₁ g₂ : β →ᵈ γ} {f : α →ᵈ β} (hf : Surjective f) :
    g₁.comp f = g₂.comp f ↔ g₁ = g₂ :=
  ⟨fun h => Dilation.ext <| hf.forall.2 (Dilation.ext_iff.1 h), fun h => h ▸ rfl⟩

Right Cancellation Property for Composition of Dilations

Informal description

Let $f \colon \alpha \to \beta$ be a surjective dilation between pseudo-emetric spaces, and let $g_1, g_2 \colon \beta \to \gamma$ be dilations. Then the composition $g_1 \circ f$ equals $g_2 \circ f$ if and only if $g_1 = g_2$.

Dilation.cancel_left theorem

{g : β →ᵈ γ} {f₁ f₂ : α →ᵈ β} (hg : Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂

Full source

@[simp]
theorem cancel_left {g : β →ᵈ γ} {f₁ f₂ : α →ᵈ β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => Dilation.ext fun x => hg <| by rw [← comp_apply, h, comp_apply], fun h => h ▸ rfl⟩

Left Cancellation Property for Composition of Dilations

Informal description

Let $g \colon \beta \to \gamma$ be an injective dilation between pseudo-emetric spaces, and let $f_1, f_2 \colon \alpha \to \beta$ be dilations. Then the composition $g \circ f_1$ equals $g \circ f_2$ if and only if $f_1 = f_2$.

Dilation.isUniformInducing theorem

: IsUniformInducing (f : α → β)

Full source

/-- A dilation from a metric space is a uniform inducing map -/
theorem isUniformInducing : IsUniformInducing (f : α → β) :=
  (antilipschitz f).isUniformInducing (lipschitz f).uniformContinuous

Dilations are Uniformly Inducing Maps

Informal description

A dilation $f \colon \alpha \to \beta$ between pseudo-extended metric spaces is a uniform inducing map, meaning the uniformity filter on $\alpha$ is the pullback of the uniformity filter on $\beta$ under the product map $f \times f$.

Dilation.tendsto_nhds_iff theorem

 {ι : Type*} {g : ι → α} {a : Filter ι} {b : α} :
  Filter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto ((f : α → β) ∘ g) a (𝓝 (f b))

Full source

theorem tendsto_nhds_iff {ι : Type*} {g : ι → α} {a : Filter ι} {b : α} :
    Filter.TendstoFilter.Tendsto g a (𝓝 b) ↔ Filter.Tendsto ((f : α → β) ∘ g) a (𝓝 (f b)) :=
  (Dilation.isUniformInducing f).isInducing.tendsto_nhds_iff

Characterization of Limits via Dilations: $\lim g = b \leftrightarrow \lim (f \circ g) = f(b)$

Informal description

Let $f \colon \alpha \to \beta$ be a dilation between pseudo-extended metric spaces. For any function $g \colon \iota \to \alpha$, filter $a$ on $\iota$, and point $b \in \alpha$, the function $g$ tends to $b$ along $a$ if and only if the composition $f \circ g$ tends to $f(b)$ along $a$. In other words, $\lim_{a} g = b$ if and only if $\lim_{a} (f \circ g) = f(b)$.

Dilation.toContinuous theorem

: Continuous (f : α → β)

Full source

/-- A dilation is continuous. -/
theorem toContinuous : Continuous (f : α → β) :=
  (lipschitz f).continuous

Continuity of Dilations

Informal description

Every dilation $f \colon \alpha \to \beta$ between pseudo-extended metric spaces is continuous.

Dilation.ediam_image theorem

(s : Set α) : EMetric.diam ((f : α → β) '' s) = ratio f * EMetric.diam s

Full source

/-- Dilations scale the diameter by `ratio f` in pseudoemetric spaces. -/
theorem ediam_image (s : Set α) : EMetric.diam ((f : α → β) '' s) = ratio f * EMetric.diam s := by
  refine ((lipschitz f).ediam_image_le s).antisymm ?_
  apply ENNReal.mul_le_of_le_div'
  rw [div_eq_mul_inv, mul_comm, ← ENNReal.coe_inv]
  exacts [(antilipschitz f).le_mul_ediam_image s, ratio_ne_zero f]

Dilation Scales Diameter: $\text{diam}(f(s)) = r \cdot \text{diam}(s)$

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-extended metric spaces and any subset $s \subseteq \alpha$, the diameter of the image $f(s)$ satisfies $\text{diam}(f(s)) = r \cdot \text{diam}(s)$, where $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0} \setminus \{0\}$ is the dilation ratio of $f$.

Dilation.ediam_range theorem

: EMetric.diam (range (f : α → β)) = ratio f * EMetric.diam (univ : Set α)

Full source

/-- A dilation scales the diameter of the range by `ratio f`. -/
theorem ediam_range : EMetric.diam (range (f : α → β)) = ratio f * EMetric.diam (univ : Set α) := by
  rw [← image_univ]; exact ediam_image f univ

Dilation Scales Range Diameter: $\text{diam}(\text{range}(f)) = r \cdot \text{diam}(\text{univ})$

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudo-extended metric spaces, the diameter of the range of $f$ equals the product of the dilation ratio $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0} \setminus \{0\}$ and the diameter of the universal set in $\alpha$. That is, \[ \text{diam}(\text{range}(f)) = r \cdot \text{diam}(\text{univ}). \]

Dilation.mapsTo_emetric_ball theorem

(x : α) (r : ℝ≥0∞) : MapsTo (f : α → β) (EMetric.ball x r) (EMetric.ball (f x) (ratio f * r))

Full source

/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/
theorem mapsTo_emetric_ball (x : α) (r : ℝ≥0∞) :
    MapsTo (f : α → β) (EMetric.ball x r) (EMetric.ball (f x) (ratio f * r)) :=
  fun y hy => (edist_eq f y x).trans_lt <|
    (ENNReal.mul_lt_mul_left (ENNReal.coe_ne_zero.2 <| ratio_ne_zero f) ENNReal.coe_ne_top).2 hy

Dilation Maps Open Balls to Scaled Open Balls

Informal description

Let $f \colon \alpha \to \beta$ be a dilation between pseudo-extended metric spaces with ratio $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0} \setminus \{0\}$. For any point $x \in \alpha$ and radius $R \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the function $f$ maps the open ball $B(x, R)$ in $\alpha$ to the open ball $B(f(x), r \cdot R)$ in $\beta$. That is, \[ f(B(x, R)) \subseteq B(f(x), r \cdot R). \]

Dilation.mapsTo_emetric_closedBall theorem

(x : α) (r' : ℝ≥0∞) : MapsTo (f : α → β) (EMetric.closedBall x r') (EMetric.closedBall (f x) (ratio f * r'))

Full source

/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/
theorem mapsTo_emetric_closedBall (x : α) (r' : ℝ≥0∞) :
    MapsTo (f : α → β) (EMetric.closedBall x r') (EMetric.closedBall (f x) (ratio f * r')) :=
  fun y hy => (edist_eq f y x).trans_le <| mul_le_mul_left' hy _

Dilation Maps Closed Balls to Scaled Closed Balls

Informal description

Let $\alpha$ and $\beta$ be pseudo-extended metric spaces, and let $f : \alpha \to \beta$ be a dilation with ratio $r \in \mathbb{R}_{\geq 0} \setminus \{0\}$. For any point $x \in \alpha$ and any radius $r' \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the dilation $f$ maps the closed ball $\overline{B}(x, r')$ in $\alpha$ to the closed ball $\overline{B}(f(x), r \cdot r')$ in $\beta$. That is, \[ f\left(\overline{B}(x, r')\right) \subseteq \overline{B}(f(x), r \cdot r'). \]

Dilation.comp_continuousOn_iff theorem

{γ} [TopologicalSpace γ] {g : γ → α} {s : Set γ} : ContinuousOn ((f : α → β) ∘ g) s ↔ ContinuousOn g s

Full source

theorem comp_continuousOn_iff {γ} [TopologicalSpace γ] {g : γ → α} {s : Set γ} :
    ContinuousOnContinuousOn ((f : α → β) ∘ g) s ↔ ContinuousOn g s :=
  (Dilation.isUniformInducing f).isInducing.continuousOn_iff.symm

Continuity of Composition with Dilation on Subset

Informal description

Let $\gamma$ be a topological space, $g \colon \gamma \to \alpha$ a function, and $s \subseteq \gamma$ a subset. For a dilation $f \colon \alpha \to \beta$, the composition $f \circ g$ is continuous on $s$ if and only if $g$ is continuous on $s$.

Dilation.comp_continuous_iff theorem

{γ} [TopologicalSpace γ] {g : γ → α} : Continuous ((f : α → β) ∘ g) ↔ Continuous g

Full source

theorem comp_continuous_iff {γ} [TopologicalSpace γ] {g : γ → α} :
    ContinuousContinuous ((f : α → β) ∘ g) ↔ Continuous g :=
  (Dilation.isUniformInducing f).isInducing.continuous_iff.symm

Continuity of Composition with Dilation

Informal description

Let $\alpha$ and $\beta$ be pseudo-extended metric spaces, and let $f \colon \alpha \to \beta$ be a dilation. For any topological space $\gamma$ and any function $g \colon \gamma \to \alpha$, the composition $f \circ g$ is continuous if and only if $g$ is continuous.

Dilation.isUniformEmbedding theorem

[PseudoEMetricSpace β] [DilationClass F α β] (f : F) : IsUniformEmbedding f

Full source

/-- A dilation from a metric space is a uniform embedding -/
lemma isUniformEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) :
    IsUniformEmbedding f :=
  (antilipschitz f).isUniformEmbedding (lipschitz f).uniformContinuous

Dilations are Uniform Embeddings

Informal description

Let $\alpha$ and $\beta$ be pseudo-extended metric spaces, and let $f \colon \alpha \to \beta$ be a dilation (i.e., there exists $r \in \mathbb{R}_{\geq 0} \setminus \{0, \infty\}$ such that for all $x, y \in \alpha$, the extended distance satisfies $\text{edist}(f(x), f(y)) = r \cdot \text{edist}(x, y)$). Then $f$ is a uniform embedding.

Dilation.isEmbedding theorem

[PseudoEMetricSpace β] [DilationClass F α β] (f : F) : IsEmbedding (f : α → β)

Full source

/-- A dilation from a metric space is an embedding -/
theorem isEmbedding [PseudoEMetricSpace β] [DilationClass F α β] (f : F) :
    IsEmbedding (f : α → β) :=
  (Dilation.isUniformEmbedding f).isEmbedding

Dilations are Topological Embeddings

Informal description

Let $\alpha$ and $\beta$ be pseudo-extended metric spaces, and let $f \colon \alpha \to \beta$ be a dilation (i.e., there exists $r \in \mathbb{R}_{\geq 0} \setminus \{0, \infty\}$ such that for all $x, y \in \alpha$, the extended distance satisfies $\text{edist}(f(x), f(y)) = r \cdot \text{edist}(x, y)$). Then $f$ is a topological embedding.

Dilation.isClosedEmbedding theorem

[CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) : IsClosedEmbedding f

Full source

/-- A dilation from a complete emetric space is a closed embedding -/
lemma isClosedEmbedding [CompleteSpace α] [EMetricSpace β] [DilationClass F α β] (f : F) :
    IsClosedEmbedding f :=
  (antilipschitz f).isClosedEmbedding (lipschitz f).uniformContinuous

Closed Embedding Property of Dilations from Complete Extended Metric Spaces

Informal description

Let $\alpha$ be a complete extended metric space and $\beta$ an extended metric space. For any dilation $f \colon \alpha \to \beta$ (i.e., a map satisfying $\text{edist}(f(x), f(y)) = r \cdot \text{edist}(x, y)$ for some $r \in \mathbb{R}_{>0}$), the function $f$ is a closed embedding. That is, $f$ is injective, continuous, and maps closed sets in $\alpha$ to closed sets in $\beta$ (relative to the subspace topology on the image of $f$).

Dilation.ratio_comp theorem

 [MetricSpace α] [Nontrivial α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β} :
  ratio (g.comp f) = ratio g * ratio f

Full source

/-- 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. -/
@[simp]
theorem ratio_comp [MetricSpace α] [Nontrivial α] [PseudoEMetricSpace β]
    [PseudoEMetricSpace γ] {g : β →ᵈ γ} {f : α →ᵈ β} : ratio (g.comp f) = ratio g * ratio f :=
  ratio_comp' <|
    let ⟨x, y, hne⟩ := exists_pair_ne α; ⟨x, y, mt edist_eq_zero.1 hne, edist_ne_top _ _⟩

Ratio of Composition of Dilations is Product of Ratios

Informal description

Let $\alpha$ be a nontrivial metric space, and $\beta$, $\gamma$ be pseudo-emetric spaces. For any dilations $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the ratio of their composition $g \circ f$ is the product of their ratios, i.e., \[ \text{ratio}(g \circ f) = \text{ratio}(g) \cdot \text{ratio}(f). \]

Dilation.diam_image theorem

(s : Set α) : Metric.diam ((f : α → β) '' s) = ratio f * Metric.diam s

Full source

/-- A dilation scales the diameter by `ratio f` in pseudometric spaces. -/
theorem diam_image (s : Set α) : Metric.diam ((f : α → β) '' s) = ratio f * Metric.diam s := by
  simp [Metric.diam, ediam_image, ENNReal.toReal_mul]

Dilation Scales Diameter: $\text{diam}(f(s)) = r \cdot \text{diam}(s)$

Informal description

For any dilation $f \colon \alpha \to \beta$ between pseudometric spaces and any subset $s \subseteq \alpha$, the diameter of the image $f(s)$ satisfies $\text{diam}(f(s)) = r \cdot \text{diam}(s)$, where $r = \text{ratio}(f) \in \mathbb{R}_{>0}$ is the dilation ratio of $f$.

Dilation.diam_range theorem

: Metric.diam (range (f : α → β)) = ratio f * Metric.diam (univ : Set α)

Full source

theorem diam_range : Metric.diam (range (f : α → β)) = ratio f * Metric.diam (univ : Set α) := by
  rw [← image_univ, diam_image]

Dilation Scales Range Diameter: $\text{diam}(\text{range}(f)) = r \cdot \text{diam}(\text{univ})$

Informal description

For a dilation $f \colon \alpha \to \beta$ between pseudometric spaces, the diameter of the range of $f$ equals the product of the dilation ratio $r = \text{ratio}(f) \in \mathbb{R}_{>0}$ and the diameter of the universal set in $\alpha$, i.e., \[ \text{diam}(\text{range}(f)) = r \cdot \text{diam}(\text{univ}). \]

Dilation.mapsTo_ball theorem

(x : α) (r' : ℝ) : MapsTo (f : α → β) (Metric.ball x r') (Metric.ball (f x) (ratio f * r'))

Full source

/-- A dilation maps balls to balls and scales the radius by `ratio f`. -/
theorem mapsTo_ball (x : α) (r' : ℝ) :
    MapsTo (f : α → β) (Metric.ball x r') (Metric.ball (f x) (ratio f * r')) :=
  fun y hy => (dist_eq f y x).trans_lt <| (mul_lt_mul_left <| NNReal.coe_pos.2 <| ratio_pos f).2 hy

Dilation Maps Open Balls to Scaled Open Balls

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation with ratio $r = \text{ratio}(f) > 0$. For any point $x \in \alpha$ and radius $r' > 0$, the dilation $f$ maps the open ball $\text{ball}(x, r')$ in $\alpha$ to the open ball $\text{ball}(f(x), r \cdot r')$ in $\beta$. That is, for every $y \in \text{ball}(x, r')$, we have $f(y) \in \text{ball}(f(x), r \cdot r')$.

Dilation.mapsTo_sphere theorem

(x : α) (r' : ℝ) : MapsTo (f : α → β) (Metric.sphere x r') (Metric.sphere (f x) (ratio f * r'))

Full source

/-- A dilation maps spheres to spheres and scales the radius by `ratio f`. -/
theorem mapsTo_sphere (x : α) (r' : ℝ) :
    MapsTo (f : α → β) (Metric.sphere x r') (Metric.sphere (f x) (ratio f * r')) :=
  fun y hy => Metric.mem_sphere.mp hy ▸ dist_eq f y x

Dilation Maps Spheres to Scaled Spheres

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation with ratio $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0}$. For any point $x \in \alpha$ and radius $r' \geq 0$, the dilation $f$ maps the sphere $\text{sphere}(x, r')$ in $\alpha$ to the sphere $\text{sphere}(f(x), r \cdot r')$ in $\beta$. In other words, for every $y \in \text{sphere}(x, r')$, we have $f(y) \in \text{sphere}(f(x), r \cdot r')$.

Dilation.mapsTo_closedBall theorem

(x : α) (r' : ℝ) : MapsTo (f : α → β) (Metric.closedBall x r') (Metric.closedBall (f x) (ratio f * r'))

Full source

/-- A dilation maps closed balls to closed balls and scales the radius by `ratio f`. -/
theorem mapsTo_closedBall (x : α) (r' : ℝ) :
    MapsTo (f : α → β) (Metric.closedBall x r') (Metric.closedBall (f x) (ratio f * r')) :=
  fun y hy => (dist_eq f y x).trans_le <| mul_le_mul_of_nonneg_left hy (NNReal.coe_nonneg _)

Dilation Maps Closed Balls to Scaled Closed Balls

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f : \alpha \to \beta$ be a dilation with ratio $r = \text{ratio}(f) \in \mathbb{R}_{\geq 0}$. For any point $x \in \alpha$ and radius $r' \geq 0$, the dilation $f$ maps the closed ball $\overline{B}(x, r')$ in $\alpha$ to the closed ball $\overline{B}(f(x), r \cdot r')$ in $\beta$. In other words, for every $y \in \overline{B}(x, r')$, we have $f(y) \in \overline{B}(f(x), r \cdot r')$.

Dilation.tendsto_cobounded theorem

: Filter.Tendsto f (cobounded α) (cobounded β)

Full source

lemma tendsto_cobounded : Filter.Tendsto f (cobounded α) (cobounded β) :=
  (Dilation.antilipschitz f).tendsto_cobounded

Dilation Preserves Co-boundedness

Informal description

Let $\alpha$ and $\beta$ be pseudometric spaces, and let $f \colon \alpha \to \beta$ be a dilation. Then $f$ maps co-bounded sets in $\alpha$ to co-bounded sets in $\beta$, i.e., the function $f$ tends to co-boundedness in the sense that for any co-bounded set $S \subseteq \alpha$, the image $f(S)$ is co-bounded in $\beta$.

Dilation.comap_cobounded theorem

: Filter.comap f (cobounded β) = cobounded α

Full source

@[simp]
lemma comap_cobounded : Filter.comap f (cobounded β) = cobounded α :=
  le_antisymm (lipschitz f).comap_cobounded_le (tendsto_cobounded f).le_comap

Dilation Preserves Co-boundedness via Preimage: $\text{comap}\, f\, (\text{cobounded}\, \beta) = \text{cobounded}\, \alpha$

Informal description

Let $f : \alpha \to \beta$ be a dilation between pseudometric spaces. Then the preimage of the co-bounded filter on $\beta$ under $f$ is equal to the co-bounded filter on $\alpha$. In other words, for any subset $S \subseteq \beta$, $S$ has bounded complement in $\beta$ if and only if $f^{-1}(S)$ has bounded complement in $\alpha$.

Mathlib.Topology.MetricSpace.Dilation

Main definitions

Notation

Implementation notes

TODO

References