dist_smul₀
theorem dist_smul₀ :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedDivisionRing α] [inst_1 : SeminormedAddCommGroup β]
[inst_2 : Module α β] [inst_3 : BoundedSMul α β] (s : α) (x y : β), dist (s • x) (s • y) = ‖s‖ * dist x y
This theorem, `dist_smul₀`, states that for any Normed Division Ring `α`, Seminormed Additive Commutative Group `β`, and given `β` is a module over `α` with bounded scalar multiplication, the distance between two vectors `x` and `y` in `β` when scaled by a scalar `s` from `α` is equal to the product of the norm of the scalar `s` and the original distance between `x` and `y`. In mathematical terms, for all `s`, `x`, and `y`, `dist (s • x) (s • y) = ‖s‖ * dist x y`.
More concisely: For any Normed Division Ring `α`, Seminormed Additive Commutative Group `β` as an `α`-module with bounded scalar multiplication, the distance between scaled vectors `dist (s • x) (s • y)` equals the product of the norm of the scalar `‖s‖` and the original distance between `x` and `y` `(dist (s • x) (s • y) = ‖s‖ * dist x y)`.
|
BoundedSMul.of_norm_smul_le
theorem BoundedSMul.of_norm_smul_le :
∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedRing α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : Module α β],
(∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) → BoundedSMul α β
This theorem states that for any types `α` and `β`, where `α` is a seminormed ring, `β` is a seminormed additive commutative group, and `β` is a module over `α`, if for every `r` in `α` and `x` in `β`, the norm of the product `r • x` is less than or equal to the product of the norms `‖r‖` and `‖x‖`, then `α` and `β` have the property `BoundedSMul`. In other words, if the norm of the scaled vector doesn't exceed the product of the norms of the scaler and the vector, then scalar multiplication is bounded in the vector space `β` with scalars from `α`.
More concisely: If `α` is a seminormed ring and `β` is a seminormed additive commutative group that is a module over `α`, then `α` and `β` have the property `BoundedSMul` if and only if for all `r` in `α` and `x` in `β`, `‖r • x‖ ≤ ‖r‖ * ‖x‖`.
|
norm_smul_le
theorem norm_smul_le :
∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
[inst_2 : SMulZeroClass α β] [inst_3 : BoundedSMul α β] (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
This theorem, `norm_smul_le`, states that for any types `α` and `β` that are seminormed add groups, along with `α` having a scalar multiplication by zero class and being bounded by `β`, for any elements `r` of type `α` and `x` of type `β`, the norm of the scalar multiplication of `r` and `x` (`r • x`) is less than or equal to the product of the norms of `r` and `x` (`‖r‖ * ‖x‖`). This is essentially a generalization of the triangle inequality to seminormed groups and scalar multiplication.
More concisely: For any seminormed add groups `α` and `β` with scalar multiplication by zero and bounded by `β`, and for any `r` in `α` and `x` in `β`, the norm of their scalar multiplication `‖r • x‖` is less than or equal to the product of the norms of `r` and `x` (`‖r‖ * ‖x‖`).
|
lipschitzWith_smul
theorem lipschitzWith_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
[inst_2 : SMulZeroClass α β] [inst_3 : BoundedSMul α β] (s : α), LipschitzWith ‖s‖₊ fun x => s • x
The theorem `lipschitzWith_smul` states that for any seminormed add groups `α` and `β` (which are types `u_1` and `u_2` respectively) that also have a multiplication operation with zero (`SMulZeroClass α β`), and the multiplication operation is bounded (`BoundedSMul α β`), for any element `s` of `α`, the function that maps `x` to `s • x` (the multiplication of `s` and `x`) is Lipschitz continuous with Lipschitz constant equal to the seminorm of `s` (`‖s‖₊`). In other words, the distance (in the sense of the edistance) between `s • x` and `s • y` is at most the seminorm of `s` times the distance between `x` and `y`, for any `x, y` in `α`.
More concisely: For any seminormed add groups `α` and `β` with multiplication operation and zero, and a bounded multiplication, the function `x mapsto s • x` is Lipschitz continuous with constant `‖s‖₊` on `α`.
|
norm_smul
theorem norm_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedDivisionRing α] [inst_1 : SeminormedAddGroup β]
[inst_2 : MulActionWithZero α β] [inst_3 : BoundedSMul α β] (r : α) (x : β), ‖r • x‖ = ‖r‖ * ‖x‖
This theorem, `norm_smul`, states that for any normed division ring `α` and any semi-normed add group `β`, if `α` multiplies `β` with zero and there exists a bounded scalar multiplication between `α` and `β`, then the norm of the scalar multiplication of any element `r` from `α` and `x` from `β` is equal to the product of the norms of `r` and `x`. In mathematical terms, for any `r` in `α` and `x` in `β`, `‖r • x‖ = ‖r‖ * ‖x‖`.
More concisely: Given a normed division ring `α` and a semi-normed add group `β` with a bounded scalar multiplication, the norm of the product of any `r` in `α` and `x` in `β` is equal to the product of the norms of `r` and `x`. That is, `‖r • x‖ = ‖r‖ * ‖x‖`.
|
nnnorm_smul_le
theorem nnnorm_smul_le :
∀ {α : Type u_1} {β : Type u_2} [inst : SeminormedAddGroup α] [inst_1 : SeminormedAddGroup β]
[inst_2 : SMulZeroClass α β] [inst_3 : BoundedSMul α β] (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊
This theorem states that for any two types α and β, where both α and β are seminormed add groups, and there exists a zero-class scalar multiplication and bounded scalar multiplication between α and β; for any elements r of type α and x of type β, the non-negative seminorm of the scalar multiplication of r and x is less than or equal to the product of the non-negative seminorms of r and x. Here, ‖r‖₊ and ‖x‖₊ denote the non-negative seminorms of r and x respectively, and r • x denotes the scalar multiplication of r and x.
More concisely: For any seminormed add groups α and β with compatible scalar multiplications, and for all elements r in α and x in β, the non-negative seminorm of their scalar product is less than or equal to the product of their non-negative seminorms: ||r • x||₊ ≤ ||r||₊ * ||x||₊.
|