# Compatibility of algebraic operations with metric space structures #

In this file we define mixin typeclasses `LipschitzMul`, `LipschitzAdd`, `IsBoundedSMul` 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 `IsUniformGroup`) is structured differently.

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

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

- lipschitz_add : ∃ (C : NNReal), LipschitzWith C fun (p : β × β) => p.1 + p.2

Instances

source
class LipschitzMul (β : Type u_2) [PseudoMetricSpace β] [Monoid β] :
Prop

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

- lipschitz_mul : ∃ (C : NNReal), LipschitzWith C fun (p : β × β) => p.1 * p.2

Instances

source
def LipschitzMul.C (β : Type u_2) [PseudoMetricSpace β] [Monoid β] [_i : LipschitzMul β] :
NNReal

The Lipschitz constant of a monoid `β` satisfying `LipschitzMul`

Equations

- LipschitzMul.C β = Classical.choose ⋯

Instances For

source
def LipschitzAdd.C (β : Type u_2) [PseudoMetricSpace β] [AddMonoid β] [_i : LipschitzAdd β] :
NNReal

The Lipschitz constant of an `AddMonoid` `β` satisfying `LipschitzAdd`

Equations

- LipschitzAdd.C β = Classical.choose ⋯

Instances For

source
theorem lipschitzWith_lipschitz_const_mul_edist {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [_i : LipschitzMul β] :
LipschitzWith (LipschitzMul.C β) fun (p : β × β) => p.1 * p.2
source
theorem lipschitzWith_lipschitz_const_add_edist {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [_i : LipschitzAdd β] :
LipschitzWith (LipschitzAdd.C β) fun (p : β × β) => p.1 + p.2
source
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
source
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
source
@[instance 100]
instance LipschitzMul.continuousMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] :
ContinuousMul β
source
@[instance 100]
instance LipschitzAdd.continuousAdd {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] :
ContinuousAdd β
source
instance Submonoid.lipschitzMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] (s : Submonoid β) :
LipschitzMul ↥s
source
instance AddSubmonoid.lipschitzAdd {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] (s : AddSubmonoid β) :
LipschitzAdd ↥s
source
instance MulOpposite.lipschitzMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] :
LipschitzMul β ᵐᵒᵖ
source
instance AddOpposite.lipschitzAdd {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] :
LipschitzAdd β ᵃᵒᵖ
source
instance Real.hasLipschitzAdd :
LipschitzAdd ℝ
source
instance NNReal.hasLipschitzAdd :
LipschitzAdd NNReal
source
class IsBoundedSMul (α : Type u_1) (β : Type u_2) [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] :
Prop

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`.

If `[NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β]` are assumed, then prefer writing `[NormSMulClass α β]` instead of using `[IsBoundedSMul α β]`, since while equivalent, typeclass search can only infer the latter from the former and not vice versa.

- dist_smul_pair' (x : α) (y₁ y₂ : β) : dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
- dist_pair_smul' (x₁ x₂ : α) (y : β) : dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Instances

source
theorem dist_smul_pair {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] (x : α) (y₁ y₂ : β) :
dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
source
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] (x₁ x₂ : α) (y : β) :
dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
source
@[instance 100]
instance IsBoundedSMul.continuousSMul {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] :
ContinuousSMul α β

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

source
@[instance 100]
instance IsBoundedSMul.toUniformContinuousConstSMul {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] :
UniformContinuousConstSMul α β
source
instance Real.isBoundedSMul :
IsBoundedSMul ℝ ℝ
source
instance NNReal.isBoundedSMul :
IsBoundedSMul NNReal NNReal
source
instance IsBoundedSMul.op {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] [SMul α ᵐᵒᵖ β] [IsCentralScalar α β] :
IsBoundedSMul α ᵐᵒᵖ β

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

source
instance instLipschitzAddAdditiveOfLipschitzMul (α : Type u_1) [PseudoMetricSpace α] [Monoid α] [LipschitzMul α] :
LipschitzAdd (Additive α)
source
instance instLipschitzMulMultiplicativeOfLipschitzAdd (α : Type u_1) [PseudoMetricSpace α] [AddMonoid α] [LipschitzAdd α] :
LipschitzMul (Multiplicative α)
source
instance instLipschitzMulOrderDual (α : Type u_1) [PseudoMetricSpace α] [Monoid α] [LipschitzMul α] :
LipschitzMul α ᵒᵈ
source
instance instLipschitzAddOrderDual (α : Type u_1) [PseudoMetricSpace α] [AddMonoid α] [LipschitzAdd α] :
LipschitzAdd α ᵒᵈ
source
instance Pi.instIsBoundedSMul {ι : Type u_3} [Fintype ι] {α : Type u_4} {β : ι → Type u_5} [PseudoMetricSpace α] [(i : ι) → PseudoMetricSpace (β i)] [Zero α] [(i : ι) → Zero (β i)] [(i : ι) → SMul α (β i)] [∀ (i : ι), IsBoundedSMul α (β i)] :
IsBoundedSMul α ((i : ι) → β i)
source
instance Pi.instIsBoundedSMul' {ι : 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 : ι), IsBoundedSMul (α i) (β i)] :
IsBoundedSMul ((i : ι) → α i) ((i : ι) → β i)
source
instance Prod.instIsBoundedSMul {α : Type u_4} {β : Type u_5} {γ : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] [Zero α] [Zero β] [Zero γ] [SMul α β] [SMul α γ] [IsBoundedSMul α β] [IsBoundedSMul α γ] :
IsBoundedSMul α (β × γ)
source
instance instIsBoundedSMulSeparationQuotient {α : Type u_4} {β : Type u_5} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] :
IsBoundedSMul α (SeparationQuotient β)