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 β] : Prop

• lipschitz_add : ∃ C, LipschitzWith C fun p => p.fst + p.snd

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

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

• lipschitz_mul : ∃ C, LipschitzWith C fun p => p.fst * p.snd

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

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

The Lipschitz constant of an AddMonoid β satisfying LipschitzAdd

Equations

• LipschitzAdd.C β = Classical.choose (_ : ∃ C, LipschitzWith C fun p => p.fst + p.snd)

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

The Lipschitz constant of a monoid β satisfying LipschitzMul

Equations

• LipschitzMul.C β = Classical.choose (_ : ∃ C, LipschitzWith C fun p => p.fst * p.snd)

theorem lipschitzWith_lipschitz_const_add_edist {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [_i : LipschitzAdd β] : LipschitzWith (LipschitzAdd.C β) fun p => p.fst + p.snd

theorem lipschitzWith_lipschitz_const_mul_edist {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [_i : LipschitzMul β] : LipschitzWith (LipschitzMul.C β) fun p => p.fst * p.snd

theorem lipschitz_with_lipschitz_const_add {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] (p : β × β) (q : β × β) : dist (p.fst + p.snd) (q.fst + q.snd) ≤ ↑(LipschitzAdd.C β) * dist p q

theorem lipschitz_with_lipschitz_const_mul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] (p : β × β) (q : β × β) : dist (p.fst * p.snd) (q.fst * q.snd) ≤ ↑(LipschitzMul.C β) * dist p q

theorem LipschitzAdd.continuousAdd.proof_1 {β : Type u_1} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : ContinuousAdd β

instance LipschitzAdd.continuousAdd {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : ContinuousAdd β

Equations

• @LipschitzAdd.continuousAdd = @LipschitzAdd.continuousAdd.proof_1

instance LipschitzMul.continuousMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] : ContinuousMul β

Equations

• @LipschitzMul.continuousMul = @LipschitzMul.continuousMul.proof_1

theorem AddSubmonoid.lipschitzAdd.proof_1 {β : Type u_1} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] (s : AddSubmonoid β) : LipschitzAdd { x // x ∈ s }

instance AddSubmonoid.lipschitzAdd {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] (s : AddSubmonoid β) : LipschitzAdd { x // x ∈ s }

Equations

• @AddSubmonoid.lipschitzAdd = @AddSubmonoid.lipschitzAdd.proof_1

instance Submonoid.lipschitzMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] (s : Submonoid β) : LipschitzMul { x // x ∈ s }

Equations

• @Submonoid.lipschitzMul = @Submonoid.lipschitzMul.proof_1

theorem AddOpposite.lipschitzAdd.proof_1 {β : Type u_1} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : LipschitzAdd βᵃᵒᵖ

abbrev AddOpposite.lipschitzAdd.match_1 {β : Type u_1} (motive : βᵃᵒᵖ × βᵃᵒᵖ → Prop) : (x : βᵃᵒᵖ × βᵃᵒᵖ) → ((y₁ y₂ : βᵃᵒᵖ) → motive (y₁, y₂)) → motive x

Equations

• AddOpposite.lipschitzAdd.match_1 motive x h_1 = Prod.casesOn x fun fst snd => h_1 fst snd

instance AddOpposite.lipschitzAdd {β : Type u_2} [PseudoMetricSpace β] [AddMonoid β] [LipschitzAdd β] : LipschitzAdd βᵃᵒᵖ

Equations

• @AddOpposite.lipschitzAdd = @AddOpposite.lipschitzAdd.proof_1

instance MulOpposite.lipschitzMul {β : Type u_2} [PseudoMetricSpace β] [Monoid β] [LipschitzMul β] : LipschitzMul βᵐᵒᵖ

Equations

• @MulOpposite.lipschitzMul = @MulOpposite.lipschitzMul.proof_1

instance Real.hasLipschitzAdd : LipschitzAdd ℝ

Equations

• Real.hasLipschitzAdd = Real.hasLipschitzAdd.proof_1

instance NNReal.hasLipschitzAdd : LipschitzAdd NNReal

Equations

• NNReal.hasLipschitzAdd = NNReal.hasLipschitzAdd.proof_1

class BoundedSMul (α : Type u_1) (β : Type u_2) [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] : Prop

• 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

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.

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 BoundedSMul.continuousSMul {α : Type u_1} {β : Type u_2} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [BoundedSMul α β] : ContinuousSMul α β

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

Equations

• @BoundedSMul.continuousSMul = @BoundedSMul.continuousSMul.proof_1

instance Real.boundedSMul : BoundedSMul ℝ ℝ

Equations

• Real.boundedSMul = Real.boundedSMul.proof_1

instance NNReal.boundedSMul : BoundedSMul NNReal NNReal

Equations

• NNReal.boundedSMul = NNReal.boundedSMul.proof_1

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

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

Equations

• @BoundedSMul.op = @BoundedSMul.op.proof_1

instance instLipschitzAddAdditiveInstPseudoMetricSpaceAdditiveAddMonoid (α : Type u_1) [PseudoMetricSpace α] [Monoid α] [LipschitzMul α] : LipschitzAdd (Additive α)

Equations

• instLipschitzAddAdditiveInstPseudoMetricSpaceAdditiveAddMonoid = instLipschitzAddAdditiveInstPseudoMetricSpaceAdditiveAddMonoid.proof_1

instance instLipschitzMulMultiplicativeInstPseudoMetricSpaceMultiplicativeMonoid (α : Type u_1) [PseudoMetricSpace α] [AddMonoid α] [LipschitzAdd α] : LipschitzMul (Multiplicative α)

Equations

• instLipschitzMulMultiplicativeInstPseudoMetricSpaceMultiplicativeMonoid = instLipschitzMulMultiplicativeInstPseudoMetricSpaceMultiplicativeMonoid.proof_1

instance instLipschitzAddOrderDualInstPseudoMetricSpaceOrderDualInstAddMonoidOrderDual (α : Type u_1) [PseudoMetricSpace α] [AddMonoid α] [LipschitzAdd α] : LipschitzAdd αᵒᵈ

Equations

• (_ : LipschitzAdd αᵒᵈ) = inst

instance instLipschitzMulOrderDualInstPseudoMetricSpaceOrderDualInstMonoidOrderDual (α : Type u_1) [PseudoMetricSpace α] [Monoid α] [LipschitzMul α] : LipschitzMul αᵒᵈ

Equations

• (_ : LipschitzMul αᵒᵈ) = 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

• @Pi.instBoundedSMul = @Pi.instBoundedSMul.proof_1

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

• @Pi.instBoundedSMul' = @Pi.instBoundedSMul'.proof_1

instance Prod.instBoundedSMul {α : Type u_4} {β : Type u_5} {γ : Type u_6} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] [Zero α] [Zero β] [Zero γ] [SMul α β] [SMul α γ] [BoundedSMul α β] [BoundedSMul α γ] : BoundedSMul α (β × γ)

Equations

• @Prod.instBoundedSMul = @Prod.instBoundedSMul.proof_1