dist_smul_pair
theorem dist_smul_pair :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
[inst_3 : Zero β] [inst_4 : SMul α β] [inst_5 : BoundedSMul α β] (x : α) (y₁ y₂ : β),
dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
This theorem states that for any two values `y1` and `y2` of type `β`, and a value `x` of type `α`, in a context where `α` and `β` are pseudo-metric spaces with zero elements and a bounded scalar multiplication operation, the distance between `x` scaled by `y1` and `x` scaled by `y2` is less than or equal to the product of the distance from `x` to zero and the distance from `y1` to `y2`. In mathematical terms, this can be represented as `dist(x*y1, x*y2) ≤ dist(x, 0) * dist(y1, y2)`.
More concisely: In a pseudo-metric space with zero elements and bounded scalar multiplication, the distance between `x` scaled by `y1` and `x` scaled by `y2` (for any `x` of type `α` and `y1`, `y2` of type `β`) is less than or equal to the product of the distance from `x` to zero and the distance from `y1` to `y2`. In symbols: `dist(x * y1, x * y2) ≤ dist(x, 0) * dist(y1, y2)`.
|
lipschitzWith_lipschitz_const_mul_edist
theorem lipschitzWith_lipschitz_const_mul_edist :
∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : Monoid β] [_i : LipschitzMul β],
LipschitzWith (LipschitzMul.C β) fun p => p.1 * p.2
This theorem states that for any type `β` which has a structure of a pseudometric space and a monoid, and also satisfies the `LipschitzMul` property, the function that takes a pair of elements `(p.1, p.2)` in `β` and multiplies them (i.e., `p.1 * p.2`) is Lipschitz continuous in the pseudometric sense. The Lipschitz constant for this function is given by `LipschitzMul.C β`, the Lipschitz constant associated with the `LipschitzMul` structure of `β`.
More concisely: Given a type `β` equipped with both a pseudometric and a monoid structure satisfying the `LipschitzMul` property, the multiplication function is Lipschitz continuous with constant `LipschitzMul.C β`.
|
dist_pair_smul
theorem dist_pair_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
[inst_3 : Zero β] [inst_4 : SMul α β] [inst_5 : BoundedSMul α β] (x₁ x₂ : α) (y : β),
dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
This theorem, `dist_pair_smul`, is a general property statement about pseudo-metric spaces. Given two types `α` and `β`, where `α` and `β` are both pseudo-metric spaces and `α` is a zero and `β` is a zero, and there exists a scalar multiplication operation "smul" as well as a bounded scalar multiplication between `α` and `β`. Then for all elements `x₁` and `x₂` in `α` and an element `y` in `β`, the distance after scalar multiplication of `x₁` and `y` to `x₂` and `y` is at most the product of the distance between `x₁` and `x₂` and the distance of `y` to zero. This could be seen as a kind of triangle inequality for scalar multiplication in pseudo-metric spaces.
More concisely: Given pseudo-metric spaces `α` and `β` with zero elements `0α` and `0β`, and a bounded scalar multiplication "smul" between them, for all `x₁, x₂ ∈ α` and `y ∈ β`, the distance `d(x₁ smul y, x₂ smul y) ≤ d(x₁, x₂) * d(y, 0β)`.
|
lipschitzWith_lipschitz_const_add_edist
theorem lipschitzWith_lipschitz_const_add_edist :
∀ {β : Type u_2} [inst : PseudoMetricSpace β] [inst_1 : AddMonoid β] [_i : LipschitzAdd β],
LipschitzWith (LipschitzAdd.C β) fun p => p.1 + p.2
The theorem `lipschitzWith_lipschitz_const_add_edist` states that for any type `β` that has a structure of a `PseudoMetricSpace`, an `AddMonoid`, and satisfies the `LipschitzAdd` condition, the function that takes a pair of elements and adds them is Lipschitz continuous with the Lipschitz constant given by `LipschitzAdd.C β`. In other words, the distance (as measured by the extended metric `edist`) between the sums of two pairs of elements in `β` is at most `LipschitzAdd.C β` times the distance between the pairs themselves.
More concisely: For any type `β` with structures of a PseudoMetricSpace and an AddMonoid satisfying the LipschitzAdd condition, the function `β => λ (x y : β), x + y` is Lipschitz continuous with Lipschitz constant `LipschitzAdd.C β` with respect to the extended metric `edist`.
|