Documentation

Mathlib.Analysis.Normed.MulAction

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 : β) :
theorem nnnorm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [IsBoundedSMul α β] (r : α) (x : β) :
theorem enorm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedAddGroup α] [SeminormedAddGroup β] [SMulZeroClass α β] [IsBoundedSMul α β] {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

Left multiplication is bounded.

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) :
theorem IsBoundedSMul.of_enorm_smul_le {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddCommGroup β] [Module α β] (h : ∀ (r : α) (x : β), r x‖ₑ r‖ₑ * x‖ₑ) :
@[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) :

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‖₊) :
@[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‖₊) :

Alias of IsBoundedSMul.of_nnnorm_smul_le.

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

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

Instances
    theorem norm_smul {α : Type u_1} {β : Type u_2} [Norm α] [Norm β] [SMul α β] [NormSMulClass α β] (r : α) (x : β) :
    @[instance 100]
    instance NormMulClass.toNormSMulClass {α : Type u_1} [Norm α] [Mul α] [NormMulClass α] :
    class ENormSMulClass (α : Type u_3) (β : Type u_4) [ENorm α] [ENorm β] [SMul α β] :

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

    Instances
      theorem enorm_smul {α : Type u_1} {β : Type u_2} [ENorm α] [ENorm β] [SMul α β] [ENormSMulClass α β] (r : α) (x : β) :
      theorem NormSMulClass.of_nnnorm_smul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] (h : ∀ (r : α) (x : β), r x‖₊ = r‖₊ * x‖₊) :
      theorem nnnorm_smul {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] [NormSMulClass α β] (r : α) (x : β) :
      @[instance 100]
      instance instENormSMulClass {α : Type u_1} {β : Type u_2} [SeminormedRing α] [SeminormedAddGroup β] [SMul α β] [NormSMulClass α β] :
      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 α (β × γ)
      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

      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.