Documentation

Mathlib.Topology.MetricSpace.Dilation

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 #

Notation #

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 #

References #

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 : αβ
  • edist_eq' : ∃ (r : NNReal), r 0 ∀ (x y : α), edist (self.toFun x) (self.toFun y) = r * edist x y
Instances For
    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.

    Instances
      instance Dilation.funLike {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] :
      FunLike (α →ᵈ β) α β
      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 β] :
      CoeFun (α →ᵈ β) fun (x : α →ᵈ β) => αβ
      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 : α →ᵈ β} :
      f = g ∀ (x : α), f x = g x
      @[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
      Instances For
        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
        Instances For
          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 = ) :
          theorem Dilation.ratio_of_subsingleton {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [Subsingleton α] [DilationClass F α β] (f : F) :
          theorem Dilation.ratio_ne_zero {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :
          theorem Dilation.ratio_pos {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : 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) :

          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) :

          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) :

          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
          Instances For
            @[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) :
            @[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) :
            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
            Instances For
              @[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) :
              @[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) :
              @[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
              Instances For
                @[simp]
                theorem Isometry.toDilation_ratio {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] {f : αβ} {hf : Isometry f} :
                theorem Dilation.lipschitz {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [FunLike F α β] [DilationClass F α β] (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

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

                The identity is a dilation

                Equations
                Instances For
                  Equations
                  • Dilation.instInhabitedDilation = { default := Dilation.id α }
                  @[simp]
                  theorem Dilation.coe_id {α : Type u_1} [PseudoEMetricSpace α] :
                  (Dilation.id α) = 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
                  Instances For
                    theorem Dilation.comp_assoc {α : Type u_1} {β : Type u_2} {γ : Type u_3} [PseudoEMetricSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] {δ : Type u_6} [PseudoEMetricSpace δ] (f : α →ᵈ β) (g : β →ᵈ γ) (h : γ →ᵈ δ) :
                    @[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 ) :

                    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 : α →ᵈ β) :
                    @[simp]
                    theorem Dilation.id_comp {α : Type u_1} {β : Type u_2} [PseudoEMetricSpace α] [PseudoEMetricSpace β] (f : α →ᵈ β) :
                    Equations
                    • Dilation.instMonoidDilation = Monoid.mk npowRec
                    theorem Dilation.mul_def {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (g : α →ᵈ α) :
                    f * g = Dilation.comp f g
                    @[simp]
                    theorem Dilation.coe_one {α : Type u_1} [PseudoEMetricSpace α] :
                    1 = id
                    @[simp]
                    theorem Dilation.coe_mul {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (g : α →ᵈ α) :
                    (f * g) = f g
                    @[simp]
                    @[simp]
                    theorem Dilation.ratio_mul {α : Type u_1} [PseudoEMetricSpace α] (f : α →ᵈ α) (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' := }
                    Instances For
                      @[simp]
                      theorem Dilation.ratio_pow {α : Type u_1} [PseudoEMetricSpace α] (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) :

                      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 α) :

                      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) :

                      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) :

                      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 γ} :
                      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 : γα} :
                      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) :

                      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 : α →ᵈ β} :

                      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 α) :

                      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) :
                      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' : ) :

                      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) :
                      @[simp]
                      theorem Dilation.comap_cobounded {α : Type u_1} {β : Type u_2} {F : Type u_4} [PseudoMetricSpace α] [PseudoMetricSpace β] [FunLike F α β] [DilationClass F α β] (f : F) :