# 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) [] :

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

Instances
class LipschitzMul (β : Type u_2) [] :

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

Instances
def LipschitzAdd.C (β : Type u_2) [] [_i : ] :

The Lipschitz constant of an AddMonoid β satisfying LipschitzAdd

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

The Lipschitz constant of a monoid β satisfying LipschitzMul

Instances For
theorem lipschitzWith_lipschitz_const_add_edist {β : Type u_2} [] [_i : ] :
LipschitzWith () fun p => p.fst + p.snd
theorem lipschitzWith_lipschitz_const_mul_edist {β : Type u_2} [] [_i : ] :
LipschitzWith () fun p => p.fst * p.snd
theorem lipschitz_with_lipschitz_const_add {β : Type u_2} [] [] (p : β × β) (q : β × β) :
dist (p.fst + p.snd) (q.fst + q.snd) ↑() * dist p q
theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [] [] (p : β × β) (q : β × β) :
dist (p.fst * p.snd) (q.fst * q.snd) ↑() * dist p q
instance LipschitzMul.continuousMul {β : Type u_2} [] [] :
theorem AddSubmonoid.lipschitzAdd.proof_1 {β : Type u_1} [] [] (s : ) :
LipschitzAdd { x // x s }
instance AddSubmonoid.lipschitzAdd {β : Type u_2} [] [] (s : ) :
LipschitzAdd { x // x s }
instance Submonoid.lipschitzMul {β : Type u_2} [] [] (s : ) :
LipschitzMul { x // x s }
abbrev AddOpposite.lipschitzAdd.match_1 {β : Type u_1} (motive : βᵃᵒᵖ × βᵃᵒᵖProp) :
(x : βᵃᵒᵖ × βᵃᵒᵖ) → ((y₁ y₂ : βᵃᵒᵖ) → motive (y₁, y₂)) → motive x
Instances For
instance MulOpposite.lipschitzMul {β : Type u_2} [] [] :
class BoundedSMul (α : Type u_1) (β : Type u_2) [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 dist_smul_pair {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMul α β] [] (x : α) (y₁ : β) (y₂ : β) :
dist (x y₁) (x y₂) dist x 0 * dist y₁ y₂
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMul α β] [] (x₁ : α) (x₂ : α) (y : β) :
dist (x₁ y) (x₂ y) dist x₁ x₂ * dist y 0
instance BoundedSMul.continuousSMul {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMul α β] [] :

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

instance BoundedSMul.op {α : Type u_1} {β : Type u_2} [Zero α] [Zero β] [SMul α β] [] [SMul αᵐᵒᵖ β] [] :

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

instance Pi.instBoundedSMul {ι : Type u_3} [] {α : Type u_4} {β : ιType u_5} [(i : ι) → PseudoMetricSpace (β i)] [Zero α] [(i : ι) → Zero (β i)] [(i : ι) → SMul α (β i)] [∀ (i : ι), BoundedSMul α (β i)] :
BoundedSMul α ((i : ι) → β i)
instance Pi.instBoundedSMul' {ι : Type u_3} [] {α : ι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)
instance Prod.instBoundedSMul {α : Type u_4} {β : Type u_5} {γ : Type u_6} [Zero α] [Zero β] [Zero γ] [SMul α β] [SMul α γ] [] [] :
BoundedSMul α (β × γ)