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.

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.

@[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

@[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‖

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

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.

@[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)

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.

@[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

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‖

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‖

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

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.

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.

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)

@[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‖

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

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.

@[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)

@[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

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.)

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.

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.

@[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

theorem ContinuousLinearMap.comp_lsmul_flip_apply {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [SeminormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : f.comp ((lsmul 𝕜 𝕜).flip x) = (lsmul 𝕜 𝕜).flip (f x)

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

theorem ContinuousLinearMap.norm_toSpanSingleton (𝕜 : Type u_1) {E : Type u_2} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) : ‖toSpanSingleton 𝕜 x‖ = ‖x‖

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‖

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.

@[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

@[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

@[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.