mathlib3 documentation

topology.metric_space.algebra

Compatibility of algebraic operations with metric space structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define mixin typeclasses has_lipschitz_mul, has_lipschitz_add, has_bounded_smul 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 has_continuous_mul instance from has_lipschitz_mul, etc. In principle there should be an intermediate typeclass for uniform spaces, but the algebraic hierarchy there (see uniform_group) is structured differently.

source
@[class]
structure has_lipschitz_add (β : Type u_2) [pseudo_metric_space β] [add_monoid β] :
Prop

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

Instances of this typeclass
source
@[class]
structure has_lipschitz_mul (β : Type u_2) [pseudo_metric_space β] [monoid β] :
Prop

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

Instances of this typeclass
source
noncomputable def has_lipschitz_add.C (β : Type u_2) [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :
nnreal

The Lipschitz constant of an add_monoid β satisfying has_lipschitz_add

Equations
source
noncomputable def has_lipschitz_mul.C (β : Type u_2) [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] :
nnreal

The Lipschitz constant of a monoid β satisfying has_lipschitz_mul

Equations
source
theorem lipschitz_with_lipschitz_const_mul_edist {β : Type u_2} [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] :
lipschitz_with (has_lipschitz_mul.C β) (λ (p : β × β), p.fst * p.snd)
source
theorem lipschitz_with_lipschitz_const_add_edist {β : Type u_2} [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :
lipschitz_with (has_lipschitz_add.C β) (λ (p : β × β), p.fst + p.snd)
source
theorem lipschitz_with_lipschitz_const_add {β : Type u_2} [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] (p q : β × β) :
has_dist.dist (p.fst + p.snd) (q.fst + q.snd) ≤ ↑(has_lipschitz_add.C β) * has_dist.dist p q
source
theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] (p q : β × β) :
has_dist.dist (p.fst * p.snd) (q.fst * q.snd) ≤ ↑(has_lipschitz_mul.C β) * has_dist.dist p q
source
@[protected, instance]
def has_lipschitz_add.has_continuous_add {β : Type u_2} [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :
has_continuous_add β
source
@[protected, instance]
def has_lipschitz_mul.has_continuous_mul {β : Type u_2} [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] :
has_continuous_mul β
source
@[protected, instance]
def submonoid.has_lipschitz_mul {β : Type u_2} [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] (s : submonoid β) :
has_lipschitz_mul ↥s
source
@[protected, instance]
def add_submonoid.has_lipschitz_add {β : Type u_2} [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] (s : add_submonoid β) :
has_lipschitz_add ↥s
source
@[protected, instance]
def add_opposite.has_lipschitz_add {β : Type u_2} [pseudo_metric_space β] [add_monoid β] [has_lipschitz_add β] :
has_lipschitz_add βᵃᵒᵖ
source
@[protected, instance]
def mul_opposite.has_lipschitz_mul {β : Type u_2} [pseudo_metric_space β] [monoid β] [has_lipschitz_mul β] :
has_lipschitz_mul βᵐᵒᵖ
source
@[protected, instance]
def real.has_lipschitz_add  :
has_lipschitz_add ℝ
source
@[protected, instance]
def nnreal.has_lipschitz_add  :
has_lipschitz_add nnreal
source
@[class]
structure has_bounded_smul (α : Type u_1) (β : Type u_2) [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_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.

Instances of this typeclass
source
theorem dist_smul_pair {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] [has_bounded_smul α β] (x : α) (y₁ y₂ : β) :
has_dist.dist (x • y₁) (x • y₂) ≤ has_dist.dist x 0 * has_dist.dist y₁ y₂
source
theorem dist_pair_smul {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] [has_bounded_smul α β] (x₁ x₂ : α) (y : β) :
has_dist.dist (x₁ • y) (x₂ • y) ≤ has_dist.dist x₁ x₂ * has_dist.dist y 0
source
@[protected, instance]
def has_bounded_smul.has_continuous_smul {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] [has_bounded_smul α β] :
has_continuous_smul α β

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

source
@[protected, instance]
def real.has_bounded_smul  :
has_bounded_smul ℝ ℝ
source
@[protected, instance]
def nnreal.has_bounded_smul  :
has_bounded_smul nnreal nnreal
source
@[protected, instance]
def has_bounded_smul.op {α : Type u_1} {β : Type u_2} [pseudo_metric_space α] [pseudo_metric_space β] [has_zero α] [has_zero β] [has_smul α β] [has_bounded_smul α β] [has_smul αᵐᵒᵖ β] [is_central_scalar α β] :
has_bounded_smul αᵐᵒᵖ β

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

source
@[protected, instance]
def additive.has_lipschitz_add (α : Type u_1) [pseudo_metric_space α] [monoid α] [has_lipschitz_mul α] :
has_lipschitz_add (additive α)
source
@[protected, instance]
def multiplicative.has_lipschitz_mul (α : Type u_1) [pseudo_metric_space α] [add_monoid α] [has_lipschitz_add α] :
has_lipschitz_mul (multiplicative α)
source
@[protected, instance]
def order_dual.has_lipschitz_mul (α : Type u_1) [pseudo_metric_space α] [monoid α] [has_lipschitz_mul α] :
has_lipschitz_mul αᵒᵈ
source
@[protected, instance]
def order_dual.has_lipschitz_add (α : Type u_1) [pseudo_metric_space α] [add_monoid α] [has_lipschitz_add α] :
has_lipschitz_add αᵒᵈ