Documentation

Mathlib.Topology.MetricSpace.Algebra

Compatibility of algebraic operations with metric space structures #

In this file we define mixin typeclasses LipschitzMul, LipschitzAdd, BoundedSMul expressing compatibility of multiplication, addition and scalar-multiplication operations with an underlying metric space structure. The intended use case is to abstract certain properties shared by normed groups and by R≥0.

Implementation notes #

We deduce a ContinuousMul instance from LipschitzMul, etc. In principle there should be an intermediate typeclass for uniform spaces, but the algebraic hierarchy there (see UniformGroup) is structured differently.

class LipschitzAdd (β : Type u_2) [PseudoMetricSpace β] [AddMonoid β] :

Class LipschitzAdd M says that the addition (+) : X × X → X is Lipschitz jointly in the two arguments.

Instances
    theorem LipschitzAdd.lipschitz_add {β : Type u_2} :
    ∀ {inst : PseudoMetricSpace β} {inst_1 : AddMonoid β} [self : LipschitzAdd β], ∃ (C : NNReal), LipschitzWith C fun (p : β × β) => p.1 + p.2
    class LipschitzMul (β : Type u_2) [PseudoMetricSpace β] [Monoid β] :

    Class LipschitzMul M says that the multiplication (*) : X × X → X is Lipschitz jointly in the two arguments.

    Instances
      theorem LipschitzMul.lipschitz_mul {β : Type u_2} :
      ∀ {inst : PseudoMetricSpace β} {inst_1 : Monoid β} [self : LipschitzMul β], ∃ (C : NNReal), LipschitzWith C fun (p : β × β) => p.1 * p.2

      The Lipschitz constant of an AddMonoid β satisfying LipschitzAdd

      Equations
      Instances For
        def LipschitzMul.C (β : Type u_2) [PseudoMetricSpace β] [Monoid β] [_i : LipschitzMul β] :

        The Lipschitz constant of a monoid β satisfying LipschitzMul

        Equations
        Instances For
          theorem lipschitzWith_lipschitz_const_add_edist {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [_i : LipschitzAdd β] :
          LipschitzWith (LipschitzAdd.C β) fun (p : β × β) => p.1 + p.2
          theorem lipschitzWith_lipschitz_const_mul_edist {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [_i : LipschitzMul β] :
          LipschitzWith (LipschitzMul.C β) fun (p : β × β) => p.1 * p.2
          theorem lipschitz_with_lipschitz_const_add {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] (p : β × β) (q : β × β) :
          dist (p.1 + p.2) (q.1 + q.2) (LipschitzAdd.C β) * dist p q
          theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] (p : β × β) (q : β × β) :
          dist (p.1 * p.2) (q.1 * q.2) (LipschitzMul.C β) * dist p q
          @[instance 100]
          Equations
          • =
          @[instance 100]
          Equations
          • =
          Equations
          • =
          instance Submonoid.lipschitzMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] (s : Submonoid β) :
          Equations
          • =
          Equations
          • =
          class BoundedSMul (α : Type u_1) (β : Type u_2) [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] :

          Mixin typeclass on a scalar action of a metric space α on a metric space β both with distinguished points 0, requiring compatibility of the action in the sense that dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂ and dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0.

          Instances
            theorem BoundedSMul.dist_smul_pair' {α : Type u_1} {β : Type u_2} :
            ∀ {inst : PseudoMetricSpace α} {inst_1 : PseudoMetricSpace β} {inst_2 : Zero α} {inst_3 : Zero β} {inst_4 : SMul α β} [self : BoundedSMul α β] (x : α) (y₁ y₂ : β), dist (x y₁) (x y₂) dist x 0 * dist y₁ y₂
            theorem BoundedSMul.dist_pair_smul' {α : Type u_1} {β : Type u_2} :
            ∀ {inst : PseudoMetricSpace α} {inst_1 : PseudoMetricSpace β} {inst_2 : Zero α} {inst_3 : Zero β} {inst_4 : SMul α β} [self : BoundedSMul α β] (x₁ x₂ : α) (y : β), dist (x₁ y) (x₂ y) dist x₁ x₂ * dist y 0
            theorem dist_smul_pair {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [BoundedSMul α β] (x : α) (y₁ : β) (y₂ : β) :
            dist (x y₁) (x y₂) dist x 0 * dist y₁ y₂
            theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [BoundedSMul α β] (x₁ : α) (x₂ : α) (y : β) :
            dist (x₁ y) (x₂ y) dist x₁ x₂ * dist y 0
            @[instance 100]
            instance BoundedSMul.continuousSMul {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [BoundedSMul α β] :

            The typeclass BoundedSMul on a metric-space scalar action implies continuity of the action.

            Equations
            • =
            @[instance 100]
            Equations
            • =
            instance BoundedSMul.op {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [BoundedSMul α β] [SMul αᵐᵒᵖ β] [IsCentralScalar α β] :

            If a scalar is central, then its right action is bounded when its left action is.

            Equations
            • =
            Equations
            • = inst
            Equations
            • = inst
            instance Pi.instBoundedSMul {ι : Type u_3} [Fintype ι] {α : Type u_4} {β : ιType u_5} [PseudoMetricSpace α] [(i : ι) → PseudoMetricSpace (β i)] [Zero α] [(i : ι) → Zero (β i)] [(i : ι) → SMul α (β i)] [∀ (i : ι), BoundedSMul α (β i)] :
            BoundedSMul α ((i : ι) → β i)
            Equations
            • =
            instance Pi.instBoundedSMul' {ι : Type u_3} [Fintype ι] {α : ιType u_4} {β : ιType u_5} [(i : ι) → PseudoMetricSpace (α i)] [(i : ι) → PseudoMetricSpace (β i)] [(i : ι) → Zero (α i)] [(i : ι) → Zero (β i)] [(i : ι) → SMul (α i) (β i)] [∀ (i : ι), BoundedSMul (α i) (β i)] :
            BoundedSMul ((i : ι) → α i) ((i : ι) → β i)
            Equations
            • =
            instance Prod.instBoundedSMul {α : Type u_4} {β : Type u_5} {γ : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] [Zero α] [Zero β] [Zero γ] [SMul α β] [SMul α γ] [BoundedSMul α β] [BoundedSMul α γ] :
            BoundedSMul α (β × γ)
            Equations
            • =