Mathlib.Analysis.NormedSpace.OperatorNorm.Mul

ContinuousLinearMap.mul_apply' theorem

(x y : R) : mul 𝕜 R x y = x * y

Full source

@[simp]
theorem mul_apply' (x y : R) : mul 𝕜 R x y = x * y :=
  rfl

Multiplication Operator Application: $\mathrm{mul}_{\mathbb{K}} R\, x\, y = x * y$

Informal description

For any elements $x$ and $y$ in a normed algebra $R$ over a field $\mathbb{K}$, the operator `mul 𝕜 R x y` (representing the multiplication operator applied to $x$ and $y$) equals the product $x * y$.

ContinuousLinearMap.opNorm_mul_apply_le theorem

(x : R) : ‖mul 𝕜 R x‖ ≤ ‖x‖

Full source

@[simp]
theorem opNorm_mul_apply_le (x : R) : ‖mul 𝕜 R x‖ ≤ ‖x‖ :=
  opNorm_le_bound _ (norm_nonneg x) (norm_mul_le x)

Operator Norm Bound for Left Multiplication in Normed Algebras

Informal description

For any element $x$ in a normed algebra $R$ over a field $\mathbb{K}$, the operator norm of the left multiplication operator $\mathrm{mul}_{\mathbb{K}} R\, x$ is bounded by the norm of $x$, i.e., $\|\mathrm{mul}_{\mathbb{K}} R\, x\| \leq \|x\|$.

ContinuousLinearMap.opNorm_mul_le theorem

: ‖mul 𝕜 R‖ ≤ 1

Full source

theorem opNorm_mul_le : ‖mul 𝕜 R‖ ≤ 1 :=
  LinearMap.mkContinuous₂_norm_le _ zero_le_one _

Operator Norm Bound for Multiplication in Normed Algebras: $\|\mathrm{mul}_{\mathbb{K}} R\| \leq 1$

Informal description

The operator norm of the multiplication operator $\mathrm{mul}_{\mathbb{K}} R$ in a normed algebra $R$ over a field $\mathbb{K}$ is bounded by $1$, i.e., $\|\mathrm{mul}_{\mathbb{K}} R\| \leq 1$.

NonUnitalAlgHom.coe_Lmul theorem

: ⇑(NonUnitalAlgHom.Lmul 𝕜 R) = mul 𝕜 R

Full source

@[simp]
theorem _root_.NonUnitalAlgHom.coe_Lmul : ⇑(NonUnitalAlgHom.Lmul 𝕜 R) = mul 𝕜 R :=
  rfl

Coefficient of Left Multiplication Homomorphism Equals Multiplication Operator

Informal description

The underlying function of the non-unital algebra homomorphism `Lmul 𝕜 R` (left multiplication by elements of `R` over the field `𝕜`) is equal to the multiplication operator `mul 𝕜 R`.

ContinuousLinearMap.mulLeftRight_apply theorem

(x y z : R) : mulLeftRight 𝕜 R x y z = x * z * y

Full source

@[simp]
theorem mulLeftRight_apply (x y z : R) : mulLeftRight 𝕜 R x y z = x * z * y :=
  rfl

Action of Left-Right Multiplication Operator: $\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\, y\, z = x z y$

Informal description

For any elements $x, y, z$ in a normed algebra $R$ over a field $\mathbb{K}$, the operator `mulLeftRight` satisfies the identity $\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\, y\, z = x * z * y$.

ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le theorem

(x y : R) : ‖mulLeftRight 𝕜 R x y‖ ≤ ‖x‖ * ‖y‖

Full source

theorem opNorm_mulLeftRight_apply_apply_le (x y : R) : ‖mulLeftRight 𝕜 R x y‖ ≤ ‖x‖ * ‖y‖ :=
  (opNorm_comp_le _ _).trans <|
    (mul_comm _ _).trans_le <|
      mul_le_mul (opNorm_mul_apply_le _ _ _)
        (opNorm_le_bound _ (norm_nonneg _) fun _ => (norm_mul_le _ _).trans_eq (mul_comm _ _))
        (norm_nonneg _) (norm_nonneg _)

Operator Norm Bound for Bilinear Multiplication in Normed Algebras: $\|\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\, y\| \leq \|x\| \cdot \|y\|$

Informal description

For any elements $x$ and $y$ in a normed algebra $R$ over a field $\mathbb{K}$, the operator norm of the bilinear operator $\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\, y$ is bounded by the product of the norms of $x$ and $y$, i.e., $\|\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\, y\| \leq \|x\| \cdot \|y\|$.

ContinuousLinearMap.opNorm_mulLeftRight_apply_le theorem

(x : R) : ‖mulLeftRight 𝕜 R x‖ ≤ ‖x‖

Full source

theorem opNorm_mulLeftRight_apply_le (x : R) : ‖mulLeftRight 𝕜 R x‖ ≤ ‖x‖ :=
  opNorm_le_bound _ (norm_nonneg x) (opNorm_mulLeftRight_apply_apply_le 𝕜 R x)

Operator Norm Bound for Left-Right Multiplication: $\|\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\| \leq \|x\|$

Informal description

For any element $x$ in a normed algebra $R$ over a field $\mathbb{K}$, the operator norm of the left-right multiplication operator $\mathrm{mulLeftRight}_{\mathbb{K}} R\, x$ is bounded by the norm of $x$, i.e., $\|\mathrm{mulLeftRight}_{\mathbb{K}} R\, x\| \leq \|x\|$.

ContinuousLinearMap.opNorm_mulLeftRight_le theorem

: ‖mulLeftRight 𝕜 R‖ ≤ 1

Full source

theorem opNorm_mulLeftRight_le :
    ‖mulLeftRight 𝕜 R‖ ≤ 1 :=
  opNorm_le_bound _ zero_le_one fun x => (one_mul ‖x‖).symm ▸ opNorm_mulLeftRight_apply_le 𝕜 R x

Operator Norm Bound for Left-Right Multiplication: $\|\mathrm{mulLeftRight}_{\mathbb{K}} R\| \leq 1$

Informal description

The operator norm of the left-right multiplication operator $\mathrm{mulLeftRight}_{\mathbb{K}} R$ in a normed algebra $R$ over a field $\mathbb{K}$ is bounded by $1$, i.e., $\|\mathrm{mulLeftRight}_{\mathbb{K}} R\| \leq 1$.

RegularNormedAlgebra structure

Full source

/-- This is a mixin class for non-unital normed algebras which states that the left-regular
representation of the algebra on itself is isometric. Every unital normed algebra with `‖1‖ = 1` is
a regular normed algebra (see `NormedAlgebra.instRegularNormedAlgebra`). In addition, so is every
C⋆-algebra, non-unital included (see `CStarRing.instRegularNormedAlgebra`), but there are yet other
examples. Any algebra with an approximate identity (e.g., $$L^1$$) is also regular.

This is a useful class because it gives rise to a nice norm on the unitization; in particular it is
a C⋆-norm when the norm on `A` is a C⋆-norm. -/
class _root_.RegularNormedAlgebra : Prop where
  /-- The left regular representation of the algebra on itself is an isometry. -/
  isometry_mul' : Isometry (mul 𝕜 R)

Regular Normed Algebra

Informal description

A non-unital normed algebra $ A $ is called *regular* if the left-regular representation of $ A $ on itself is isometric. This means that for every element $ x \in A $, the operator norm of left multiplication by $ x $ equals the norm of $ x $. This property holds for: 1. Any unital normed algebra with $ \|1\| = 1 $ 2. Any C⋆-algebra (including non-unital ones) 3. Any algebra with an approximate identity (e.g., $ L^1 $ spaces) This class is particularly useful because it induces a natural norm on the unitization of $ A $, which becomes a C⋆-norm when $ A $ itself has a C⋆-norm.

ContinuousLinearMap.isometry_mul theorem

: Isometry (mul 𝕜 R)

Full source

lemma isometry_mul : Isometry (mul 𝕜 R) :=
  RegularNormedAlgebra.isometry_mul'

Isometry of Left Multiplication in Regular Normed Algebras

Informal description

For a regular normed algebra $R$ over a field $\mathbb{K}$, the left multiplication operator $\text{mul}_{\mathbb{K}} R : R \to \mathcal{L}(R)$ is an isometry. That is, for any $x \in R$, the operator norm of left multiplication by $x$ equals the norm of $x$: $\|\text{mul}_{\mathbb{K}} R(x)\| = \|x\|$.

ContinuousLinearMap.opNorm_mul_apply theorem

(x : R) : ‖mul 𝕜 R x‖ = ‖x‖

Full source

@[simp]
lemma opNorm_mul_apply (x : R) : ‖mul 𝕜 R x‖ = ‖x‖ :=
  (AddMonoidHomClass.isometry_iff_norm (mul 𝕜 R)).mp (isometry_mul 𝕜 R) x

Operator Norm of Left Multiplication in Regular Normed Algebra Equals Element Norm

Informal description

For any element $x$ in a regular normed algebra $R$ over a field $\mathbb{K}$, the operator norm of left multiplication by $x$ equals the norm of $x$, i.e., $\|\text{mul}_{\mathbb{K}} R(x)\| = \|x\|$.

ContinuousLinearMap.opNNNorm_mul_apply theorem

(x : R) : ‖mul 𝕜 R x‖₊ = ‖x‖₊

Full source

@[simp]
lemma opNNNorm_mul_apply (x : R) : ‖mul 𝕜 R x‖₊ = ‖x‖₊ :=
  Subtype.ext <| opNorm_mul_apply 𝕜 R x

Operator Seminorm of Left Multiplication in Regular Normed Algebra Equals Element Seminorm

Informal description

For any element $x$ in a regular normed algebra $R$ over a field $\mathbb{K}$, the operator seminorm of left multiplication by $x$ equals the seminorm of $x$, i.e., $\|\text{mul}_{\mathbb{K}} R(x)\|_+ = \|x\|_+$.

ContinuousLinearMap.coe_mulₗᵢ theorem

: ⇑(mulₗᵢ 𝕜 R) = mul 𝕜 R

Full source

@[simp]
theorem coe_mulₗᵢ : ⇑(mulₗᵢ 𝕜 R) = mul 𝕜 R :=
  rfl

Underlying Function of Left Multiplication Isometry Equals Left Multiplication Map

Informal description

The underlying function of the linear isometry `mulₗᵢ 𝕜 R` (left multiplication in the regular normed algebra $R$ over the field $\mathbb{K}$) is equal to the continuous linear map `mul 𝕜 R`.

ContinuousLinearMap.flip_mul theorem

: (ContinuousLinearMap.mul 𝕜 R).flip = .mul 𝕜 R

Full source

@[simp] lemma flip_mul : (ContinuousLinearMap.mul 𝕜 R).flip = .mul 𝕜 R := by ext; simp [mul_comm]

Flip of Multiplication Map Equals Itself

Informal description

The flip of the continuous linear multiplication map $\text{mul}_{\mathbb{K}} R$ is equal to the continuous linear multiplication map $\text{mul}_{\mathbb{K}} R$ itself.

ContinuousLinearMap.lsmul_apply theorem

(c : R) (x : E) : lsmul 𝕜 R c x = c • x

Full source

@[simp]
theorem lsmul_apply (c : R) (x : E) : lsmul 𝕜 R c x = c • x :=
  rfl

Left Scalar Multiplication Equals Scalar Multiplication

Informal description

For any scalar $c$ in a normed algebra $R$ over a field $\mathbb{K}$ and any element $x$ in a normed space $E$ over $\mathbb{K}$, the application of the left scalar multiplication operator $\text{lsmul}_{\mathbb{K}} R$ to $c$ and $x$ equals the scalar multiplication $c \cdot x$.

ContinuousLinearMap.norm_toSpanSingleton theorem

(x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖

Full source

theorem norm_toSpanSingleton (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖ := by
  refine opNorm_eq_of_bounds (norm_nonneg _) (fun x => ?_) fun N _ h => ?_
  · rw [toSpanSingleton_apply, norm_smul, mul_comm]
  · specialize h 1
    rw [toSpanSingleton_apply, norm_smul, mul_comm] at h
    exact (mul_le_mul_right (by simp)).mp h

Operator Norm of Span Singleton Map Equals Element Norm: $\|\text{toSpanSingleton}_{\mathbb{K}} x\| = \|x\|$

Informal description

For any element $x$ in a normed space $E$ over a field $\mathbb{K}$, the operator norm of the linear map $\text{toSpanSingleton}_{\mathbb{K}} x$ (which sends scalars to their scalar multiples of $x$) is equal to the norm of $x$, i.e., $\|\text{toSpanSingleton}_{\mathbb{K}} x\| = \|x\|$.

ContinuousLinearMap.opNorm_lsmul_apply_le theorem

(x : R) : ‖(lsmul 𝕜 R x : E →L[𝕜] E)‖ ≤ ‖x‖

Full source

theorem opNorm_lsmul_apply_le (x : R) : ‖(lsmul 𝕜 R x : E →L[𝕜] E)‖ ≤ ‖x‖ :=
  ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg x) fun y => norm_smul_le x y

Operator Norm Bound for Left Scalar Multiplication: $\|\text{lsmul}_{\mathbb{K}} R x\| \leq \|x\|$

Informal description

Let $R$ be a normed algebra over a field $\mathbb{K}$, and let $E$ be a normed space over $\mathbb{K}$. For any element $x \in R$, the operator norm of the left scalar multiplication map $\text{lsmul}_{\mathbb{K}} R x \colon E \to E$ is bounded by the norm of $x$, i.e., $\|\text{lsmul}_{\mathbb{K}} R x\| \leq \|x\|$.

ContinuousLinearMap.opNorm_lsmul_le theorem

: ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ ≤ 1

Full source

/-- The norm of `lsmul` is at most 1 in any semi-normed group. -/
theorem opNorm_lsmul_le : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ ≤ 1 := by
  refine ContinuousLinearMap.opNorm_le_bound _ zero_le_one fun x => ?_
  simp_rw [one_mul]
  exact opNorm_lsmul_apply_le _

Operator Norm Bound for Left Scalar Multiplication: $\|\text{lsmul}_{\mathbb{K}} R\| \leq 1$

Informal description

Let $R$ be a normed algebra over a field $\mathbb{K}$ and $E$ be a normed space over $\mathbb{K}$. The operator norm of the left scalar multiplication map $\text{lsmul}_{\mathbb{K}} R \colon R \to \mathcal{L}(E, E)$ is bounded by $1$, i.e., $\|\text{lsmul}_{\mathbb{K}} R\| \leq 1$.

ContinuousLinearMap.opNorm_mul theorem

: ‖mul 𝕜 R‖ = 1

Full source

@[simp]
theorem opNorm_mul : ‖mul 𝕜 R‖ = 1 :=
  (mulₗᵢ 𝕜 R).norm_toContinuousLinearMap

Operator Norm of Multiplication Map: $\|\text{mul}_{\mathbb{K}} R\| = 1$

Informal description

Let $R$ be a normed algebra over a field $\mathbb{K}$. The operator norm of the multiplication map $\text{mul}_{\mathbb{K}} R \colon R \to \mathcal{L}(R)$ is equal to $1$, i.e., $\|\text{mul}_{\mathbb{K}} R\| = 1$.

ContinuousLinearMap.opNNNorm_mul theorem

: ‖mul 𝕜 R‖₊ = 1

Full source

@[simp]
theorem opNNNorm_mul : ‖mul 𝕜 R‖₊ = 1 :=
  Subtype.ext <| opNorm_mul 𝕜 R

Operator Seminorm of Multiplication Map: $\|\text{mul}_{\mathbb{K}} R\|_+ = 1$

Informal description

For a normed algebra $R$ over a field $\mathbb{K}$, the operator seminorm of the multiplication map $\text{mul}_{\mathbb{K}} R \colon R \to \mathcal{L}(R)$ is equal to $1$, i.e., $\|\text{mul}_{\mathbb{K}} R\|_+ = 1$.

ContinuousLinearMap.opNorm_lsmul theorem

 [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] [Nontrivial E] :
  ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ = 1

Full source

/-- The norm of `lsmul` equals 1 in any nontrivial normed group.

This is `ContinuousLinearMap.opNorm_lsmul_le` as an equality. -/
@[simp]
theorem opNorm_lsmul [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E]
    [IsScalarTower 𝕜 R E] [Nontrivial E] : ‖(lsmul 𝕜 R : R →L[𝕜] E →L[𝕜] E)‖ = 1 := by
  refine ContinuousLinearMap.opNorm_eq_of_bounds zero_le_one (fun x => ?_) fun N _ h => ?_
  · rw [one_mul]
    apply opNorm_lsmul_apply_le
  obtain ⟨y, hy⟩ := exists_ne (0 : E)
  have := le_of_opNorm_le _ (h 1) y
  simp_rw [lsmul_apply, one_smul, norm_one, mul_one] at this
  refine le_of_mul_le_mul_right ?_ (norm_pos_iff.mpr hy)
  simp_rw [one_mul, this]

Operator Norm of Left Scalar Multiplication in Nontrivial Normed Spaces: $\|\text{lsmul}_{\mathbb{K}} R\| = 1$

Informal description

Let $\mathbb{K}$ be a normed field, $R$ a normed algebra over $\mathbb{K}$, and $E$ a normed space over $\mathbb{K}$ such that $R$ acts on $E$ compatibly with $\mathbb{K}$ (i.e., $[ \mathbb{K}, R, E ]$ forms a scalar tower). If $E$ is nontrivial, then the operator norm of the left scalar multiplication map $\text{lsmul}_{\mathbb{K}} R \colon R \to \mathcal{L}(E)$ equals $1$, i.e., $\|\text{lsmul}_{\mathbb{K}} R\| = 1$.