Mathlib.Topology.MetricSpace.Algebra

LipschitzAdd structure

[AddMonoid β]

Full source

/-- Class `LipschitzAdd M` says that the addition `(+) : X × X → X` is Lipschitz jointly in
the two arguments. -/
class LipschitzAdd [AddMonoid β] : Prop where
  lipschitz_add : ∃ C, LipschitzWith C fun p : β × β => p.1 + p.2

Lipschitz continuity of addition

Informal description

The structure `LipschitzAdd` asserts that the addition operation `(+) : β × β → β` on an additive monoid `β` is Lipschitz continuous jointly in both arguments with respect to the underlying pseudometric space structure. This means there exists a constant `C` such that for any two pairs of elements `(x₁, y₁)` and `(x₂, y₂)` in `β × β`, the distance between their sums is bounded by `C` times the sum of the distances between the corresponding components.

LipschitzMul structure

[Monoid β]

Full source

/-- Class `LipschitzMul M` says that the multiplication `(*) : X × X → X` is Lipschitz jointly
in the two arguments. -/
@[to_additive]
class LipschitzMul [Monoid β] : Prop where
  lipschitz_mul : ∃ C, LipschitzWith C fun p : β × β => p.1 * p.2

Lipschitz continuity of multiplication

Informal description

The structure `LipschitzMul` asserts that the multiplication operation `(*) : β × β → β` on a monoid `β` is Lipschitz continuous jointly in both arguments with respect to the underlying pseudometric space structure. This means there exists a constant `C` such that for any two pairs of elements `(x₁, y₁)` and `(x₂, y₂)` in `β × β`, the distance between their products is bounded by `C` times the sum of the distances between the corresponding components.

LipschitzAdd.C definition

[AddMonoid β] [_i : LipschitzAdd β] : ℝ≥0

Full source

/-- The Lipschitz constant of an `AddMonoid` `β` satisfying `LipschitzAdd` -/
def LipschitzAdd.C [AddMonoid β] [_i : LipschitzAdd β] : ℝ≥0 := Classical.choose _i.lipschitz_add

Lipschitz constant for addition

Informal description

The Lipschitz constant for the addition operation on an additive monoid $\beta$ equipped with a `LipschitzAdd` instance. This constant $C$ satisfies that for any two pairs of elements $(x_1, y_1)$ and $(x_2, y_2)$ in $\beta \times \beta$, the distance between their sums is bounded by $C$ times the sum of the distances between the corresponding components.

LipschitzMul.C definition

[_i : LipschitzMul β] : ℝ≥0

Full source

/-- The Lipschitz constant of a monoid `β` satisfying `LipschitzMul` -/
@[to_additive existing] -- Porting note: had to add `LipschitzAdd.C`. to_additive silently failed
def LipschitzMul.C [_i : LipschitzMul β] : ℝ≥0 := Classical.choose _i.lipschitz_mul

Lipschitz constant for multiplication

Informal description

The constant $C$ associated with a monoid $\beta$ satisfying `LipschitzMul`, which bounds the distance between products in terms of the distances between the factors. Specifically, for any $x_1, x_2, y_1, y_2 \in \beta$, we have $\text{dist}(x_1 y_1, x_2 y_2) \leq C (\text{dist}(x_1, x_2) + \text{dist}(y_1, y_2))$.

lipschitzWith_lipschitz_const_mul_edist theorem

[_i : LipschitzMul β] : LipschitzWith (LipschitzMul.C β) fun p : β × β => p.1 * p.2

Full source

@[to_additive]
theorem lipschitzWith_lipschitz_const_mul_edist [_i : LipschitzMul β] :
    LipschitzWith (LipschitzMul.C β) fun p : β × β => p.1 * p.2 :=
  Classical.choose_spec _i.lipschitz_mul

Lipschitz continuity of multiplication with constant $C$

Informal description

For a monoid $\beta$ equipped with a pseudometric space structure and satisfying `LipschitzMul`, the multiplication operation $(x, y) \mapsto x * y$ is Lipschitz continuous with constant $C = \text{LipschitzMul.C}(\beta)$. That is, for any pairs $(x_1, y_1), (x_2, y_2) \in \beta \times \beta$, the distance between the products satisfies $\text{dist}(x_1 y_1, x_2 y_2) \leq C \cdot \text{dist}((x_1, y_1), (x_2, y_2))$.

lipschitz_with_lipschitz_const_mul theorem

: ∀ p q : β × β, dist (p.1 * p.2) (q.1 * q.2) ≤ LipschitzMul.C β * dist p q

Full source

@[to_additive]
theorem lipschitz_with_lipschitz_const_mul :
    ∀ p q : β × β, dist (p.1 * p.2) (q.1 * q.2) ≤ LipschitzMul.C β * dist p q := by
  rw [← lipschitzWith_iff_dist_le_mul]
  exact lipschitzWith_lipschitz_const_mul_edist

Lipschitz continuity of multiplication with constant $C$

Informal description

For any monoid $\beta$ equipped with a pseudometric space structure and satisfying `LipschitzMul`, the multiplication operation is Lipschitz continuous with constant $C = \text{LipschitzMul.C}(\beta)$. That is, for any pairs $(x_1, y_1), (x_2, y_2) \in \beta \times \beta$, the distance between their products satisfies $\text{dist}(x_1 y_1, x_2 y_2) \leq C \cdot \text{dist}((x_1, y_1), (x_2, y_2))$.

LipschitzMul.continuousMul instance

: ContinuousMul β

Full source

@[to_additive]
instance (priority := 100) LipschitzMul.continuousMul : ContinuousMul β :=
  ⟨lipschitzWith_lipschitz_const_mul_edist.continuous⟩

Lipschitz Multiplication Implies Continuous Multiplication

Informal description

For any monoid $\beta$ with a pseudometric space structure satisfying `LipschitzMul`, the multiplication operation on $\beta$ is jointly continuous.

Submonoid.lipschitzMul instance

(s : Submonoid β) : LipschitzMul s

Full source

@[to_additive]
instance Submonoid.lipschitzMul (s : Submonoid β) : LipschitzMul s where
  lipschitz_mul := ⟨LipschitzMul.C β, by
    rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
    convert lipschitzWith_lipschitz_const_mul_edist ⟨(x₁ : β), x₂⟩ ⟨y₁, y₂⟩ using 1⟩

Lipschitz Continuity of Multiplication in Submonoids

Informal description

For any submonoid $s$ of a monoid $\beta$ equipped with a pseudometric space structure satisfying `LipschitzMul`, the submonoid $s$ inherits the `LipschitzMul` property. This means that the multiplication operation on $s$ is Lipschitz continuous with respect to the induced pseudometric space structure.

MulOpposite.lipschitzMul instance

: LipschitzMul βᵐᵒᵖ

Full source

@[to_additive]
instance MulOpposite.lipschitzMul : LipschitzMul βᵐᵒᵖ where
  lipschitz_mul := ⟨LipschitzMul.C β, fun ⟨x₁, x₂⟩ ⟨y₁, y₂⟩ =>
    (lipschitzWith_lipschitz_const_mul_edist ⟨x₂.unop, x₁.unop⟩ ⟨y₂.unop, y₁.unop⟩).trans_eq
      (congr_arg _ <| max_comm _ _)⟩

Lipschitz Continuity of Multiplication on the Multiplicative Opposite

Informal description

The multiplicative opposite $\beta^\text{op}$ of a monoid $\beta$ with a Lipschitz continuous multiplication operation inherits the Lipschitz continuity property for its reversed multiplication. Specifically, if the multiplication on $\beta$ is Lipschitz continuous with constant $C$, then the multiplication on $\beta^\text{op}$ is also Lipschitz continuous with the same constant $C$.

Real.hasLipschitzAdd instance

: LipschitzAdd ℝ

Full source

instance Real.hasLipschitzAdd : LipschitzAdd ℝ where
  lipschitz_add := ⟨2, LipschitzWith.of_dist_le_mul fun p q => by
    simp only [Real.dist_eq, Prod.dist_eq, Prod.fst_sub, Prod.snd_sub, NNReal.coe_ofNat,
      add_sub_add_comm, two_mul]
    refine le_trans (abs_add (p.1 - q.1) (p.2 - q.2)) ?_
    exact add_le_add (le_max_left _ _) (le_max_right _ _)⟩

Lipschitz Continuity of Addition on Real Numbers

Informal description

The addition operation on the real numbers $\mathbb{R}$ is Lipschitz continuous with respect to the standard metric space structure. That is, there exists a constant $C$ such that for any $x_1, x_2, y_1, y_2 \in \mathbb{R}$, the distance between $x_1 + y_1$ and $x_2 + y_2$ is bounded by $C$ times the sum of the distances between $x_1$ and $x_2$, and between $y_1$ and $y_2$.

NNReal.hasLipschitzAdd instance

: LipschitzAdd ℝ≥0

Full source

instance NNReal.hasLipschitzAdd : LipschitzAdd ℝ≥0 where
  lipschitz_add := ⟨LipschitzAdd.C ℝ, by
    rintro ⟨x₁, x₂⟩ ⟨y₁, y₂⟩
    exact lipschitzWith_lipschitz_const_add_edist ⟨(x₁ : ℝ), x₂⟩ ⟨y₁, y₂⟩⟩

Lipschitz Continuity of Addition on Non-Negative Real Numbers

Informal description

The addition operation on the non-negative real numbers $\mathbb{R}_{\geq 0}$ is Lipschitz continuous with respect to the standard pseudometric space structure. That is, there exists a constant $C$ such that for any $x_1, x_2, y_1, y_2 \in \mathbb{R}_{\geq 0}$, the distance between $x_1 + y_1$ and $x_2 + y_2$ is bounded by $C$ times the sum of the distances between $x_1$ and $x_2$, and between $y_1$ and $y_2$.

IsBoundedSMul structure

Full source

/-- 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`. -/
class IsBoundedSMul : Prop where
  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

Bounded Scalar Multiplication

Informal description

A structure representing a scalar action of a metric space $\alpha$ on a metric space $\beta$, both with distinguished points $0$, that satisfies the following compatibility conditions: 1. For any $x \in \alpha$ and $y_1, y_2 \in \beta$, the distance between $x \cdot y_1$ and $x \cdot y_2$ is bounded by $\text{dist}(x, 0) \cdot \text{dist}(y_1, y_2)$. 2. For any $x_1, x_2 \in \alpha$ and $y \in \beta$, the distance between $x_1 \cdot y$ and $x_2 \cdot y$ is bounded by $\text{dist}(x_1, x_2) \cdot \text{dist}(y, 0)$. This structure ensures that the scalar multiplication operation is compatible with the metric space structures in a controlled way.

dist_smul_pair theorem

(x : α) (y₁ y₂ : β) : dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂

Full source

theorem dist_smul_pair (x : α) (y₁ y₂ : β) : dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂ :=
  IsBoundedSMul.dist_smul_pair' x y₁ y₂

Distance Bound for Scalar Multiplication by Fixed Element

Informal description

For any element $x$ in a pseudometric space $\alpha$ and any elements $y_1, y_2$ in a pseudometric space $\beta$ with distinguished point $0$, the distance between the scalar multiplications $x \cdot y_1$ and $x \cdot y_2$ is bounded by the product of the distance from $x$ to $0$ and the distance between $y_1$ and $y_2$, i.e., \[ \text{dist}(x \cdot y_1, x \cdot y_2) \leq \text{dist}(x, 0) \cdot \text{dist}(y_1, y_2). \]

dist_pair_smul theorem

(x₁ x₂ : α) (y : β) : dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0

Full source

theorem dist_pair_smul (x₁ x₂ : α) (y : β) : dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0 :=
  IsBoundedSMul.dist_pair_smul' x₁ x₂ y

Distance Bound for Scalar Multiplication by Pair of Elements

Informal description

For any elements $x₁, x₂$ in a pseudometric space $\alpha$ and any element $y$ in a pseudometric space $\beta$ with distinguished point $0$, the distance between the scalar multiplications $x₁ \cdot y$ and $x₂ \cdot y$ is bounded by the product of the distance between $x₁$ and $x₂$ and the distance from $y$ to $0$, i.e., \[ \text{dist}(x₁ \cdot y, x₂ \cdot y) \leq \text{dist}(x₁, x₂) \cdot \text{dist}(y, 0). \]

IsBoundedSMul.continuousSMul instance

: ContinuousSMul α β

Full source

/-- The typeclass `IsBoundedSMul` on a metric-space scalar action implies continuity of the
action. -/
instance (priority := 100) IsBoundedSMul.continuousSMul : ContinuousSMul α β where
  continuous_smul := by
    rw [Metric.continuous_iff]
    rintro ⟨a, b⟩ ε ε0
    obtain ⟨δ, δ0, hδε⟩ : ∃ δ > 0, δ * (δ + dist b 0) + dist a 0 * δ < ε := by
      have : Continuous fun δ ↦ δ * (δ + dist b 0) + dist a 0 * δ := by fun_prop
      refine ((this.tendsto' _ _ ?_).eventually (gt_mem_nhds ε0)).exists_gt
      simp
    refine ⟨δ, δ0, fun (a', b') hab' => ?_⟩
    obtain ⟨ha, hb⟩ := max_lt_iff.1 hab'
    calc dist (a' • b') (a • b)
        ≤ dist (a' • b') (a • b') + dist (a • b') (a • b) := dist_triangle ..
      _ ≤ dist a' a * dist b' 0 + dist a 0 * dist b' b :=
        add_le_add (dist_pair_smul _ _ _) (dist_smul_pair _ _ _)
      _ ≤ δ * (δ + dist b 0) + dist a 0 * δ := by
          have : dist b' 0 ≤ δ + dist b 0 := (dist_triangle _ _ _).trans <| add_le_add_right hb.le _
          gcongr
      _ < ε := hδε

Joint Continuity of Scalar Multiplication under Boundedness Conditions

Informal description

For any pseudometric spaces $\alpha$ and $\beta$ with distinguished points $0$ and a scalar multiplication operation $\cdot : \alpha \times \beta \to \beta$ that satisfies the bounded scalar multiplication properties, the scalar multiplication operation is jointly continuous in both arguments. That is, the map $(x, y) \mapsto x \cdot y$ is continuous with respect to the product topology on $\alpha \times \beta$ and the topology on $\beta$.

IsBoundedSMul.toUniformContinuousConstSMul instance

: UniformContinuousConstSMul α β

Full source

instance (priority := 100) IsBoundedSMul.toUniformContinuousConstSMul :
    UniformContinuousConstSMul α β :=
  ⟨fun c => ((lipschitzWith_iff_dist_le_mul (K := nndist c 0)).2 fun _ _ =>
    dist_smul_pair c _ _).uniformContinuous⟩

Uniform Continuity of Scalar Multiplication under Boundedness Conditions

Informal description

For any pseudometric spaces $\alpha$ and $\beta$ with distinguished points $0$ and a scalar multiplication operation $\cdot : \alpha \times \beta \to \beta$ that satisfies the bounded scalar multiplication properties, the scalar multiplication operation is uniformly continuous in the second argument. Specifically, for any fixed $x \in \alpha$, the map $y \mapsto x \cdot y$ is uniformly continuous on $\beta$.

Real.isBoundedSMul instance

: IsBoundedSMul ℝ ℝ

Full source

instance Real.isBoundedSMul : IsBoundedSMul ℝ ℝ where
  dist_smul_pair' x y₁ y₂ := by simpa [Real.dist_eq, mul_sub] using (abs_mul x (y₁ - y₂)).le
  dist_pair_smul' x₁ x₂ y := by simpa [Real.dist_eq, sub_mul] using (abs_mul (x₁ - x₂) y).le

Bounded Scalar Multiplication on Real Numbers

Informal description

The scalar multiplication operation on the real numbers $\mathbb{R}$ is compatible with its metric space structure, satisfying the bounded scalar multiplication properties. Specifically: 1. For any $x \in \mathbb{R}$ and $y_1, y_2 \in \mathbb{R}$, the distance between $x \cdot y_1$ and $x \cdot y_2$ is bounded by $|x| \cdot \text{dist}(y_1, y_2)$. 2. For any $x_1, x_2 \in \mathbb{R}$ and $y \in \mathbb{R}$, the distance between $x_1 \cdot y$ and $x_2 \cdot y$ is bounded by $\text{dist}(x_1, x_2) \cdot |y|$.

NNReal.isBoundedSMul instance

: IsBoundedSMul ℝ≥0 ℝ≥0

Full source

instance NNReal.isBoundedSMul : IsBoundedSMul ℝ≥0 ℝ≥0 where
  dist_smul_pair' x y₁ y₂ := by convert dist_smul_pair (x : ℝ) (y₁ : ℝ) y₂ using 1
  dist_pair_smul' x₁ x₂ y := by convert dist_pair_smul (x₁ : ℝ) x₂ (y : ℝ) using 1

Bounded Scalar Multiplication on Non-Negative Real Numbers

Informal description

The scalar multiplication operation on the non-negative real numbers $\mathbb{R}_{\geq 0}$ is compatible with its metric space structure, satisfying the bounded scalar multiplication properties. Specifically: 1. For any $x \in \mathbb{R}_{\geq 0}$ and $y_1, y_2 \in \mathbb{R}_{\geq 0}$, the distance between $x \cdot y_1$ and $x \cdot y_2$ is bounded by $|x| \cdot \text{dist}(y_1, y_2)$. 2. For any $x_1, x_2 \in \mathbb{R}_{\geq 0}$ and $y \in \mathbb{R}_{\geq 0}$, the distance between $x_1 \cdot y$ and $x_2 \cdot y$ is bounded by $\text{dist}(x_1, x_2) \cdot |y|$.

IsBoundedSMul.op instance

[SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsBoundedSMul αᵐᵒᵖ β

Full source

/-- If a scalar is central, then its right action is bounded when its left action is. -/
instance IsBoundedSMul.op [SMul αᵐᵒᵖ β] [IsCentralScalar α β] : IsBoundedSMul αᵐᵒᵖ β where
  dist_smul_pair' :=
    MulOpposite.rec' fun x y₁ y₂ => by simpa only [op_smul_eq_smul] using dist_smul_pair x y₁ y₂
  dist_pair_smul' :=
    MulOpposite.rec' fun x₁ =>
      MulOpposite.rec' fun x₂ y => by simpa only [op_smul_eq_smul] using dist_pair_smul x₁ x₂ y

Bounded Scalar Multiplication for Central Actions via Opposite Algebra

Informal description

For a pseudometric space $\alpha$ with a distinguished point $0$ acting on a pseudometric space $\beta$ with a distinguished point $0$, if the scalar multiplication is central (i.e., $x \cdot y = y \cdot x$ for all $x \in \alpha$ and $y \in \beta$), then the scalar multiplication by elements of the multiplicative opposite $\alpha^\text{op}$ on $\beta$ is bounded. Specifically, the distance inequalities for scalar multiplication hold when the action is through the opposite algebra.

instLipschitzAddAdditiveOfLipschitzMul instance

[Monoid α] [LipschitzMul α] : LipschitzAdd (Additive α)

Full source

instance [Monoid α] [LipschitzMul α] : LipschitzAdd (Additive α) :=
  ⟨@LipschitzMul.lipschitz_mul α _ _ _⟩

Lipschitz Addition on Additive Monoids from Lipschitz Multiplication

Informal description

For any monoid $\alpha$ with a Lipschitz continuous multiplication operation, the additive version $\text{Additive}\,\alpha$ inherits a Lipschitz continuous addition operation.

instLipschitzMulMultiplicativeOfLipschitzAdd instance

[AddMonoid α] [LipschitzAdd α] : LipschitzMul (Multiplicative α)

Full source

instance [AddMonoid α] [LipschitzAdd α] : LipschitzMul (Multiplicative α) :=
  ⟨@LipschitzAdd.lipschitz_add α _ _ _⟩

Lipschitz Continuity of Multiplication in Multiplicative Monoids from Lipschitz Addition

Informal description

For any additive monoid $\alpha$ with a Lipschitz continuous addition operation, the multiplicative monoid structure on $\alpha$ has a Lipschitz continuous multiplication operation.

instLipschitzMulOrderDual instance

[Monoid α] [LipschitzMul α] : LipschitzMul αᵒᵈ

Full source

@[to_additive]
instance [Monoid α] [LipschitzMul α] : LipschitzMul αᵒᵈ :=
  ‹LipschitzMul α›

Lipschitz Continuity of Multiplication on Order Duals

Informal description

For any monoid $\alpha$ with a Lipschitz continuous multiplication operation, the order dual $\alpha^{\mathrm{op}}$ also has a Lipschitz continuous multiplication operation.

Pi.instIsBoundedSMul instance

 {α : Type*} {β : ι → Type*} [PseudoMetricSpace α] [∀ i, PseudoMetricSpace (β i)] [Zero α] [∀ i, Zero (β i)]
  [∀ i, SMul α (β i)] [∀ i, IsBoundedSMul α (β i)] : IsBoundedSMul α (∀ i, β i)

Full source

instance Pi.instIsBoundedSMul {α : Type*} {β : ι → Type*} [PseudoMetricSpace α]
    [∀ i, PseudoMetricSpace (β i)] [Zero α] [∀ i, Zero (β i)] [∀ i, SMul α (β i)]
    [∀ i, IsBoundedSMul α (β i)] : IsBoundedSMul α (∀ i, β i) where
  dist_smul_pair' x y₁ y₂ :=
    (dist_pi_le_iff <| by positivity).2 fun _ ↦
      (dist_smul_pair _ _ _).trans <| mul_le_mul_of_nonneg_left (dist_le_pi_dist _ _ _) dist_nonneg
  dist_pair_smul' x₁ x₂ y :=
    (dist_pi_le_iff <| by positivity).2 fun _ ↦
      (dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (dist_le_pi_dist _ 0 _) dist_nonneg

Bounded Scalar Multiplication on Product of Metric Spaces

Informal description

For any pseudometric space $\alpha$ with a distinguished point $0$ and a family of pseudometric spaces $\{\beta_i\}_{i \in \iota}$ each with a distinguished point $0$, if $\alpha$ has a scalar multiplication action on each $\beta_i$ that is compatible with their metric structures (i.e., $\alpha$ is a `IsBoundedSMul` for each $\beta_i$), then $\alpha$ also has a compatible scalar multiplication action on the product space $\prod_{i \in \iota} \beta_i$.

Pi.instIsBoundedSMul' instance

 {α β : ι → Type*} [∀ 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)

Full source

instance Pi.instIsBoundedSMul' {α β : ι → Type*} [∀ 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) where
  dist_smul_pair' x y₁ y₂ :=
    (dist_pi_le_iff <| by positivity).2 fun _ ↦
      (dist_smul_pair _ _ _).trans <|
        mul_le_mul (dist_le_pi_dist _ 0 _) (dist_le_pi_dist _ _ _) dist_nonneg dist_nonneg
  dist_pair_smul' x₁ x₂ y :=
    (dist_pi_le_iff <| by positivity).2 fun _ ↦
      (dist_pair_smul _ _ _).trans <|
        mul_le_mul (dist_le_pi_dist _ _ _) (dist_le_pi_dist _ 0 _) dist_nonneg dist_nonneg

Bounded Scalar Multiplication on Product Spaces

Informal description

For any family of pseudometric spaces $\{\alpha_i\}_{i \in \iota}$ and $\{\beta_i\}_{i \in \iota}$ each with distinguished points $0$, if each $\alpha_i$ has a scalar multiplication action on $\beta_i$ that is compatible with their metric structures (i.e., each $\alpha_i$ is a `IsBoundedSMul` for $\beta_i$), then the product space $\prod_{i \in \iota} \alpha_i$ has a compatible scalar multiplication action on the product space $\prod_{i \in \iota} \beta_i$. This means that the scalar multiplication operation on the product spaces satisfies the following boundedness conditions: 1. For any $x \in \prod_i \alpha_i$ and $y_1, y_2 \in \prod_i \beta_i$, the distance between $x \cdot y_1$ and $x \cdot y_2$ is bounded by $\text{dist}(x, 0) \cdot \text{dist}(y_1, y_2)$. 2. For any $x_1, x_2 \in \prod_i \alpha_i$ and $y \in \prod_i \beta_i$, the distance between $x_1 \cdot y$ and $x_2 \cdot y$ is bounded by $\text{dist}(x_1, x_2) \cdot \text{dist}(y, 0)$.

Prod.instIsBoundedSMul instance

 {α β γ : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [PseudoMetricSpace γ] [Zero α] [Zero β] [Zero γ] [SMul α β]
  [SMul α γ] [IsBoundedSMul α β] [IsBoundedSMul α γ] : IsBoundedSMul α (β × γ)

Full source

instance Prod.instIsBoundedSMul {α β γ : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β]
    [PseudoMetricSpace γ] [Zero α] [Zero β] [Zero γ] [SMul α β] [SMul α γ] [IsBoundedSMul α β]
    [IsBoundedSMul α γ] : IsBoundedSMul α (β × γ) where
  dist_smul_pair' _x _y₁ _y₂ :=
    max_le ((dist_smul_pair _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_left _ _) dist_nonneg)
      ((dist_smul_pair _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_right _ _) dist_nonneg)
  dist_pair_smul' _x₁ _x₂ _y :=
    max_le ((dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_left _ _) dist_nonneg)
      ((dist_pair_smul _ _ _).trans <| mul_le_mul_of_nonneg_left (le_max_right _ _) dist_nonneg)

Bounded Scalar Multiplication on Product Spaces

Informal description

For any pseudometric spaces $\alpha$, $\beta$, and $\gamma$ with distinguished points $0$, if $\alpha$ has a scalar multiplication action on both $\beta$ and $\gamma$ that is compatible with their metric structures (i.e., $\alpha$ is a `IsBoundedSMul` for both $\beta$ and $\gamma$), then $\alpha$ also has a compatible scalar multiplication action on the product space $\beta \times \gamma$.

instIsBoundedSMulSeparationQuotient instance

 {α β : Type*} [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] :
  IsBoundedSMul α (SeparationQuotient β)

Full source

instance {α β : Type*}
    [PseudoMetricSpace α] [PseudoMetricSpace β] [Zero α] [Zero β] [SMul α β] [IsBoundedSMul α β] :
    IsBoundedSMul α (SeparationQuotient β) where
  dist_smul_pair' _ := Quotient.ind₂ <| dist_smul_pair _
  dist_pair_smul' _ _ := Quotient.ind <| dist_pair_smul _ _

Bounded Scalar Multiplication on Separation Quotient

Informal description

For any pseudometric spaces $\alpha$ and $\beta$ with distinguished points $0$ and a scalar multiplication operation $\cdot : \alpha \times \beta \to \beta$ that satisfies the bounded scalar multiplication properties, the separation quotient of $\beta$ inherits the bounded scalar multiplication structure from $\beta$. This means that the scalar multiplication operation on the separation quotient remains compatible with the metric space structures in a controlled way, preserving the boundedness conditions.

Implementation notes