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.
Multiplication in a non-unital normed algebra as a continuous bilinear map.
Equations
- ContinuousLinearMap.mul 𝕜 𝕜' = (LinearMap.mul 𝕜 𝕜').mkContinuous₂ 1 ⋯
Instances For
Alias of ContinuousLinearMap.opNorm_mul_apply_le
.
Alias of ContinuousLinearMap.opNorm_mul_le
.
Multiplication on the left in a non-unital normed algebra 𝕜'
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 𝕜 𝕜' = { toFun := (↑(ContinuousLinearMap.mul 𝕜 𝕜')).toFun, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯ }
Instances For
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 𝕜 𝕜' = ((ContinuousLinearMap.compL 𝕜 𝕜' 𝕜' 𝕜').comp (ContinuousLinearMap.mul 𝕜 𝕜').flip).flip.comp (ContinuousLinearMap.mul 𝕜 𝕜')
Instances For
Alias of ContinuousLinearMap.opNorm_mulLeftRight_apply_apply_le
.
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 𝕜 𝕜')
The left regular representation of the algebra on itself is an isometry.
Instances
The left regular representation of the algebra on itself is an isometry.
Every (unital) normed algebra such that ‖1‖ = 1
is a RegularNormedAlgebra
.
Equations
- ⋯ = ⋯
Alias of ContinuousLinearMap.opNorm_mul_apply
.
Alias of ContinuousLinearMap.opNNNorm_mul_apply
.
Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.
Equations
- ContinuousLinearMap.mulₗᵢ 𝕜 𝕜' = { toLinearMap := ↑(ContinuousLinearMap.mul 𝕜 𝕜'), norm_map' := ⋯ }
Instances For
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
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
Scalar multiplication as a continuous bilinear map.
Equations
- ContinuousLinearMap.lsmul 𝕜 𝕜' = (Algebra.lsmul 𝕜 𝕜 E).toLinearMap.mkContinuous₂ 1 ⋯
Instances For
The norm of lsmul
is at most 1 in any semi-normed group.
Alias of ContinuousLinearMap.opNorm_lsmul_le
.
The norm of lsmul
is at most 1 in any semi-normed group.
Alias of ContinuousLinearMap.opNorm_mul
.
Alias of ContinuousLinearMap.opNNNorm_mul
.
The norm of lsmul
equals 1 in any nontrivial normed group.
This is ContinuousLinearMap.opNorm_lsmul_le
as an equality.
Alias of ContinuousLinearMap.opNorm_lsmul
.
The norm of lsmul
equals 1 in any nontrivial normed group.
This is ContinuousLinearMap.opNorm_lsmul_le
as an equality.