Constructions of continuous linear maps between (semi-)normed spaces #
A fundamental fact about (semi-)linear maps between normed spaces over sensible fields is that
continuity and boundedness are equivalent conditions. That is, for normed spaces E
, F
, a
LinearMap
f : E →ₛₗ[σ] F
is the coercion of some ContinuousLinearMap
f' : E →SL[σ] F
, if
and only if there exists a bound C
such that for all x
, ‖f x‖ ≤ C * ‖x‖
.
We prove one direction in this file: LinearMap.mkContinuous
, boundedness implies continuity. The
other direction, ContinuousLinearMap.bound
, is deferred to a later file, where the
strong operator topology on E →SL[σ] F
is available, because it is natural to use
ContinuousLinearMap.bound
to define a norm ⨆ x, ‖f x‖ / ‖x‖
on E →SL[σ] F
and to show that
this is compatible with the strong operator topology.
This file also contains several corollaries of LinearMap.mkContinuous
: other "easy"
constructions of continuous linear maps between normed spaces.
This file is meant to be lightweight (it is imported by much of the analysis library); think twice before adding imports!
General constructions #
Construct a continuous linear map from a linear map and a bound on this linear map.
The fact that the norm of the continuous linear map is then controlled is given in
LinearMap.mkContinuous_norm_le
.
Equations
Instances For
Construct a continuous linear map from a linear map and the existence of a bound on this linear
map. If you have an explicit bound, use LinearMap.mkContinuous
instead, as a norm estimate will
follow automatically in LinearMap.mkContinuous_norm_le
.
Equations
Instances For
Construct a continuous linear equivalence from a linear equivalence together with bounds in both directions.
Equations
- LinearEquiv.toContinuousLinearEquivOfBounds e C_to C_inv h_to h_inv = ContinuousLinearEquiv.mk e
Instances For
Reinterpret a linear map 𝕜 →ₗ[𝕜] E
as a continuous linear map. This construction
is generalized to the case of any finite dimensional domain
in LinearMap.toContinuousLinearMap
.
Equations
Instances For
Homotheties #
A (semi-)linear map which is a homothety is a continuous linear map.
Since the field 𝕜
need not have ℝ
as a subfield, this theorem is not directly deducible from
the corresponding theorem about isometries plus a theorem about scalar multiplication. Likewise
for the other theorems about homotheties in this file.
Equations
- ContinuousLinearMap.ofHomothety f a hf = LinearMap.mkContinuous f a (_ : ∀ (x : E), ‖↑f x‖ ≤ a * ‖x‖)
Instances For
A linear equivalence which is a homothety is a continuous linear equivalence.
Equations
Instances For
The span of a single vector #
Given a nonzero element x
of a normed space E₁
over a field 𝕜
, the natural
continuous linear equivalence from E₁
to the span of x
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a nonzero element x
of a normed space E₁
over a field 𝕜
, the natural continuous
linear map from the span of x
to 𝕜
.