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 α β

theorem IsBoundedSMul.of_enorm_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.

class NormSMulClass (α : Type u_3) (β : Type u_4) [Norm α] [Norm β] [SMul α β] : Prop

Mixin class for scalar-multiplication actions with a strictly multiplicative norm, i.e. ‖r • x‖ = ‖r‖ * ‖x‖.

• norm_smul (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖

theorem norm_smul {α : Type u_1} {β : Type u_2} [Norm α] [Norm β] [SMul α β] [NormSMulClass α β] (r : α) (x : β) : ‖r • x‖ = ‖r‖ * ‖x‖

@[instance 100]

instance NormMulClass.toNormSMulClass {α : Type u_1} [Norm α] [Mul α] [NormMulClass α] : NormSMulClass α α

@[instance 100]

instance NormMulClass.toNormSMulClass_op {α : Type u_1} [SeminormedRing α] [NormMulClass α] : NormSMulClass αᵐᵒᵖ α

theorem NormSMulClass.of_nnnorm_smul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] (h : ∀ (r : α) (x : β), ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊) : NormSMulClass α β

theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] [NormSMulClass α β] (r : α) (x : β) : ‖r • x‖₊ = ‖r‖₊ * ‖x‖₊

theorem enorm_smul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] [NormSMulClass α β] (r : α) (x : β) : ‖r • x‖ₑ = ‖r‖ₑ * ‖x‖ₑ

instance Pi.instNormSMulClass {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [Fintype ι] [SeminormedRing α] [(i : ι) → SeminormedAddGroup (β i)] [(i : ι) → SMul α (β i)] [∀ (i : ι), NormSMulClass α (β i)] : NormSMulClass α ((i : ι) → β i)

instance Prod.instNormSMulClass {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] [NormSMulClass α β] {γ : Type u_3} [SeminormedAddGroup γ] [SMul α γ] [NormSMulClass α γ] : NormSMulClass α (β × γ)

instance ULift.instNormSMulClass {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] [NormSMulClass α β] : NormSMulClass α (ULift.{u_3, u_2} β)

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

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

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

instance NormSMulClass.toIsBoundedSMul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddCommGroup β] [Module α β] [NormSMulClass α β] : IsBoundedSMul α β

theorem NormedDivisionRing.toNormSMulClass {α : Type u_1} {β : Type u_2} [NormedDivisionRing α] [SeminormedAddGroup β] [MulActionWithZero α β] [IsBoundedSMul α β] : NormSMulClass α β

For a normed division ring, a sub-multiplicative norm is actually strictly multiplicative.

This is not an instance as it forms a loop with NormSMulClass.toIsBoundedSMul.