Lemmas for BoundedSMul over normed additive groups

Lemmas which hold only in NormedSpace α β are provided in another file.

Notably we prove that NonUnitalSeminormedRings have bounded actions by left- and right- multiplication. This allows downstream files to write general results about BoundedSMul, and then deduce const_mul and mul_const results as an immediate corollary.

theorem norm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [BoundedSMul α β] (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖

theorem nnnorm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [BoundedSMul α β] (r : α) (x : β) : ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊

theorem dist_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [BoundedSMul α β] (s : α) (x y : β) : dist (s • x) (s • y) ≤ ‖s‖ * dist x y

theorem nndist_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [BoundedSMul α β] (s : α) (x y : β) : nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y

theorem lipschitzWith_smul {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [BoundedSMul α β] (s : α) : LipschitzWith ‖s‖₊ fun (x : β) => s • x

theorem edist_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [BoundedSMul α β] (s : α) (x y : β) : edist (s • x) (s • y) ≤ ‖s‖₊ • edist x y

instance NonUnitalSeminormedRing.to_boundedSMul {α : Type u_1} [NonUnitalSeminormedRing α] : BoundedSMul α α

Left multiplication is bounded.

instance NonUnitalSeminormedRing.to_has_bounded_op_smul {α : Type u_1} [NonUnitalSeminormedRing α] : BoundedSMul αᵐᵒᵖ α

Right multiplication is bounded.

theorem BoundedSMul.of_norm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddCommGroup β] [Module α β] (h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖) : BoundedSMul α β

theorem BoundedSMul.of_nnnorm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddCommGroup β] [Module α β] (h : ∀ (r : α) (x : β), ‖r • x‖₊ ≤ ‖r‖₊ * ‖x‖₊) : BoundedSMul α β

theorem norm_smul {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddGroup β] [MulActionWithZero α β] [BoundedSMul α β] (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖

theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddGroup β] [MulActionWithZero α β] [BoundedSMul α β] (r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊

theorem dist_smul₀ {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] [BoundedSMul α β] (s : α) (x y : β) : dist (s • x) (s • y) = ‖s‖ * dist x y

theorem nndist_smul₀ {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] [BoundedSMul α β] (s : α) (x y : β) : nndist (s • x) (s • y) = ‖s‖₊ * nndist x y

theorem edist_smul₀ {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddCommGroup β] [Module α β] [BoundedSMul α β] (s : α) (x y : β) : edist (s • x) (s • y) = ‖s‖₊ • edist x y