Operator norm for maps on normed spaces #
This file contains statements about operator norm for which it really matters that the underlying space has a norm (rather than just a seminorm).
LinearMap.bound_of_ball_bound'
is a version of this lemma over a field satisfying RCLike
that produces a concrete bound.
An operator is zero iff its norm vanishes.
Alias of ContinuousLinearMap.opNorm_zero_iff
.
An operator is zero iff its norm vanishes.
If a normed space is non-trivial, then the norm of the identity equals 1
.
Equations
- โฏ = โฏ
Continuous linear maps themselves form a normed space with respect to the operator norm.
Equations
- ContinuousLinearMap.toNormedAddCommGroup = NormedAddCommGroup.ofSeparation โฏ
Continuous linear maps form a normed ring with respect to the operator norm.
Equations
- ContinuousLinearMap.toNormedRing = NormedRing.mk โฏ โฏ
If a continuous linear map is a topology embedding, then it is expands the distances by a positive factor.
Postcomposition of a continuous linear map with a linear isometry preserves the operator norm.
Composing on the left with a linear isometry gives a linear isometry between spaces of continuous linear maps.
Equations
Instances For
Precomposition with a linear isometry preserves the operator norm.
Alias of ContinuousLinearMap.opNorm_comp_linearIsometryEquiv
.
Precomposition with a linear isometry preserves the operator norm.
A bounded bilinear form B
in a real normed space is coercive
if there is some positive constant C such that C * โuโ * โuโ โค B u u
.
Instances For
Equivalent characterizations for equicontinuity of a family of continuous linear maps
between normed spaces. See also WithSeminorms.equicontinuous_TFAE
for similar characterizations
between spaces satisfying WithSeminorms
.