# Results about operator norms in normed algebras #

This file (split off from `OperatorNorm.lean`) contains results about the operator norm of multiplication and scalar-multiplication operations in normed algebras and normed modules.

source
noncomputable def ContinuousLinearMap.mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
R →L[𝕜] R →L[𝕜] R

Multiplication in a non-unital normed algebra as a continuous bilinear map.

Equations

- ContinuousLinearMap.mul 𝕜 R = (LinearMap.mul 𝕜 R).mkContinuous₂ 1 ⋯

Instances For

source
@[simp]
theorem ContinuousLinearMap.mul_apply' (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] (x y : R) :
((mul 𝕜 R) x) y = x * y
source
@[simp]
theorem ContinuousLinearMap.opNorm_mul_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] (x : R) :
‖(mul 𝕜 R) x‖ ≤ ‖x‖
source
theorem ContinuousLinearMap.opNorm_mul_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
‖mul 𝕜 R‖ ≤ 1
source
noncomputable def NonUnitalAlgHom.Lmul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
R →ₙₐ[𝕜] R →L[𝕜] R

Multiplication on the left in a non-unital normed algebra `R` as a non-unital algebra homomorphism into the algebra of continuous linear maps. This is the left regular representation of `A` acting on itself.

This has more algebraic structure than `ContinuousLinearMap.mul`, but there is no longer continuity bundled in the first coordinate. An alternative viewpoint is that this upgrades `NonUnitalAlgHom.lmul` from a homomorphism into linear maps to a homomorphism into continuous linear maps.

Equations

- NonUnitalAlgHom.Lmul 𝕜 R = { toFun := (↑(ContinuousLinearMap.mul 𝕜 R)).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }

Instances For

source
@[simp]
theorem NonUnitalAlgHom.coe_Lmul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_3} [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
⇑(Lmul 𝕜 R) = ⇑(ContinuousLinearMap.mul 𝕜 R)
source
noncomputable def ContinuousLinearMap.mulLeftRight (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
R →L[𝕜] R →L[𝕜] R →L[𝕜] R

Simultaneous left- and right-multiplication in a non-unital normed algebra, considered as a continuous trilinear map. This is akin to its non-continuous version `LinearMap.mulLeftRight`, but there is a minor difference: `LinearMap.mulLeftRight` is uncurried.

Equations

- ContinuousLinearMap.mulLeftRight 𝕜 R = ((ContinuousLinearMap.compL 𝕜 R R R).comp (ContinuousLinearMap.mul 𝕜 R).flip).flip.comp (ContinuousLinearMap.mul 𝕜 R)

Instances For

source
@[simp]
theorem ContinuousLinearMap.mulLeftRight_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] (x y z : R) :
(((mulLeftRight 𝕜 R) x) y) z = x * z * y
source
theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] (x y : R) :
‖((mulLeftRight 𝕜 R) x) y‖ ≤ ‖x‖ * ‖y‖
source
theorem ContinuousLinearMap.opNorm_mulLeftRight_apply_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] (x : R) :
‖(mulLeftRight 𝕜 R) x‖ ≤ ‖x‖
source
theorem ContinuousLinearMap.opNorm_mulLeftRight_le (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
‖mulLeftRight 𝕜 R‖ ≤ 1
source
class RegularNormedAlgebra (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
Prop

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.

- isometry_mul' : Isometry ⇑(ContinuousLinearMap.mul 𝕜 R)

  The left regular representation of the algebra on itself is an isometry.

Instances

source
instance NormedAlgebra.instRegularNormedAlgebra {𝕜 : Type u_4} {R : Type u_5} [NontriviallyNormedField 𝕜] [SeminormedRing R] [NormedAlgebra 𝕜 R] [NormOneClass R] :
RegularNormedAlgebra 𝕜 R

Every (unital) normed algebra such that `‖1‖ = 1` is a `RegularNormedAlgebra`.

source
theorem ContinuousLinearMap.isometry_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] :
Isometry ⇑(mul 𝕜 R)
source
@[simp]
theorem ContinuousLinearMap.opNorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] (x : R) :
‖(mul 𝕜 R) x‖ = ‖x‖
source
@[simp]
theorem ContinuousLinearMap.opNNNorm_mul_apply (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] (x : R) :
‖(mul 𝕜 R) x‖₊ = ‖x‖₊
source
noncomputable def ContinuousLinearMap.mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] :
R →ₗᵢ[𝕜] R →L[𝕜] R

Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.

Equations

- ContinuousLinearMap.mulₗᵢ 𝕜 R = { toLinearMap := ↑(ContinuousLinearMap.mul 𝕜 R), norm_map' := ⋯ }

Instances For

source
@[simp]
theorem ContinuousLinearMap.coe_mulₗᵢ (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalSeminormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] :
⇑(mulₗᵢ 𝕜 R) = ⇑(mul 𝕜 R)
source
@[simp]
theorem ContinuousLinearMap.flip_mul {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {R : Type u_3} [NonUnitalSeminormedCommRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] :
(mul 𝕜 R).flip = mul 𝕜 R
source
noncomputable def ContinuousLinearMap.ring_lmap_equiv_selfₗ (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
(𝕜 →L[𝕜] E) ≃ₗ[𝕜] E

If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly equivalent to `M`. (See `ring_lmap_equiv_self` for a stronger statement.)

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
noncomputable def ContinuousLinearMap.ring_lmap_equiv_self (𝕜 : Type u_1) (E : Type u_2) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
(𝕜 →L[𝕜] E) ≃ₗᵢ[𝕜] E

If `M` is a normed space over `𝕜`, then the space of maps `𝕜 →L[𝕜] M` is linearly isometrically equivalent to `M`.

Equations

- ContinuousLinearMap.ring_lmap_equiv_self 𝕜 E = { toLinearEquiv := ContinuousLinearMap.ring_lmap_equiv_selfₗ 𝕜 E, norm_map' := ⋯ }

Instances For

source
noncomputable def ContinuousLinearMap.lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (R : Type u_3) [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] :
R →L[𝕜] E →L[𝕜] E

Scalar multiplication as a continuous bilinear map.

Equations

- ContinuousLinearMap.lsmul 𝕜 R = (Algebra.lsmul 𝕜 𝕜 E).toLinearMap.mkContinuous₂ 1 ⋯

Instances For

source
@[simp]
theorem ContinuousLinearMap.lsmul_apply (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (R : Type u_3) [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] (c : R) (x : E) :
((lsmul 𝕜 R) c) x = c • x
source
@[simp]
theorem ContinuousLinearMap.lsmul_flip_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) :
(lsmul 𝕜 𝕜).flip x = toSpanSingleton 𝕜 x
source
@[deprecated ContinuousLinearMap.comp_toSpanSingleton (since := "29-08-2025")]
theorem ContinuousLinearMap.comp_lsmul_flip_apply {R₁ : Type u_1} [Semiring R₁] {M₁ : Type u_4} [TopologicalSpace M₁] [AddCommMonoid M₁] {M₂ : Type u_6} [TopologicalSpace M₂] [AddCommMonoid M₂] [Module R₁ M₁] [Module R₁ M₂] [TopologicalSpace R₁] [ContinuousSMul R₁ M₂] [ContinuousSMul R₁ M₁] (f : M₁ →L[R₁] M₂) (x : M₁) :
f.comp (toSpanSingleton R₁ x) = toSpanSingleton R₁ (f x)

Alias of `ContinuousLinearMap.comp_toSpanSingleton`.

source
theorem ContinuousLinearMap.lsmul_flip_inj {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (R : Type u_3) [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] {x y : E} :
(lsmul 𝕜 R).flip x = (lsmul 𝕜 R).flip y ↔ x = y
source
theorem ContinuousLinearMap.norm_toSpanSingleton (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) :
‖toSpanSingleton 𝕜 x‖ = ‖x‖
source
theorem ContinuousLinearMap.opNorm_lsmul_apply_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_3} [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] (x : R) :
‖(lsmul 𝕜 R) x‖ ≤ ‖x‖
source
theorem ContinuousLinearMap.opNorm_lsmul_le {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {R : Type u_3} [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] :
‖lsmul 𝕜 R‖ ≤ 1

The norm of `lsmul` is at most 1 in any semi-normed group.

source
@[simp]
theorem ContinuousLinearMap.opNorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalNormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] [Nontrivial R] :
‖mul 𝕜 R‖ = 1
source
@[simp]
theorem ContinuousLinearMap.opNNNorm_mul (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (R : Type u_3) [NonUnitalNormedRing R] [NormedSpace 𝕜 R] [IsScalarTower 𝕜 R R] [SMulCommClass 𝕜 R R] [RegularNormedAlgebra 𝕜 R] [Nontrivial R] :
‖mul 𝕜 R‖₊ = 1
source
@[simp]
theorem ContinuousLinearMap.opNorm_lsmul (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] (R : Type u_3) [NormedField R] [NormedAlgebra 𝕜 R] [NormedSpace R E] [IsScalarTower 𝕜 R E] [Nontrivial E] :
‖lsmul 𝕜 R‖ = 1

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

This is `ContinuousLinearMap.opNorm_lsmul_le` as an equality.