Lemmas for IsBoundedSMul 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 IsBoundedSMul, 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 α β] [IsBoundedSMul α β] (r : α) (x : β) : ‖r • x‖ ≤ ‖r‖ * ‖x‖

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

theorem enorm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [IsBoundedSMul α β] {r : α} {x : β} : ‖r • x‖ₑ ≤ ‖r‖ₑ * ‖x‖ₑ

theorem dist_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [IsBoundedSMul α β] (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 α β] [IsBoundedSMul α β] (s : α) (x y : β) : nndist (s • x) (s • y) ≤ ‖s‖₊ * nndist x y

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

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

instance NonUnitalSeminormedRing.isBoundedSMul {α : Type u_1} [NonUnitalSeminormedRing α] : IsBoundedSMul α α

Left multiplication is bounded.

instance NonUnitalSeminormedRing.isBoundedSMulOpposite {α : Type u_1} [NonUnitalSeminormedRing α] : IsBoundedSMul αᵐᵒᵖ α

Right multiplication is bounded.

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

@[deprecated IsBoundedSMul.of_norm_smul_le (since := "2025-03-10")]

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

Alias of IsBoundedSMul.of_norm_smul_le.

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

@[deprecated IsBoundedSMul.of_nnnorm_smul_le (since := "2025-03-10")]

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

Alias of IsBoundedSMul.of_nnnorm_smul_le.

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

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

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

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

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

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