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 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
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
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
The typeclass BoundedSMul
on a metric-space scalar action implies continuity of the action.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
If a scalar is central, then its right action is bounded when its left action is.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = inst
Equations
- ⋯ = inst
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯