Operator norm on the space of continuous linear maps #
Define the operator norm on the space of continuous linear maps between normed spaces, and prove its basic properties. In particular, show that this space is itself a normed space.
Since a lot of elementary properties don't require ∥x∥ = 0 → x = 0
we start setting up the
theory for semi_normed_space
and we specialize to normed_space
at the end.
Most statements in this file require the field to be non-discrete,
as this is necessary to deduce an inequality ∥f x∥ ≤ C ∥x∥
from the continuity of f.
However, the other direction always holds.
In this section, we just assume that 𝕜
is a normed field.
In the remainder of the file, it will be non-discrete.
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
linear_map.mk_continuous_norm_le
.
Equations
- f.mk_continuous C h = {to_linear_map := f, cont := _}
Reinterpret a linear map 𝕜 →ₗ[𝕜] E
as a continuous linear map. This construction
is generalized to the case of any finite dimensional domain
in linear_map.to_continuous_linear_map
.
Equations
- f.to_continuous_linear_map₁ = f.mk_continuous ∥⇑f 1∥ _
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 linear_map.mk_continuous
instead, as a norm estimate will
follow automatically in linear_map.mk_continuous_norm_le
.
Equations
- f.mk_continuous_of_exists_bound h = {to_linear_map := f, cont := _}
- _ = _
If ∥x∥ = 0
and f
is continuous then ∥f x∥ = 0
.
A continuous linear map between seminormed spaces is bounded when the field is nondiscrete. The
continuity ensures boundedness on a ball of some radius ε
. The nondiscreteness is then used to
rescale any element into an element of norm in [ε/C, ε]
, whose image has a controlled norm. The
norm control for the original element follows by rescaling.
A 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
- continuous_linear_map.of_homothety f a hf = f.mk_continuous a _
Given an element x
of a normed space E
over a field 𝕜
, the natural continuous
linear map from E
to the span of x
.
Equations
The operator norm of a continuous linear map is the inf of all its bounds.
Equations
The fundamental property of the operator norm: ∥f x∥ ≤ ∥f∥ * ∥x∥
.
continuous linear maps are Lipschitz continuous.
The image of the unit ball under a continuous linear map is bounded.
If one controls the norm of every A x
, then one controls the norm of A
.
The operator norm satisfies the triangle inequality.
The norm of the 0
operator is 0
.
The norm of the identity is at most 1
. It is in fact 1
, except when the space is trivial
where it is 0
. It means that one can not do better than an inequality in general.
If there is an element with norm different from 0
, then the norm of the identity equals 1
.
(Since we are working with seminorms supposing that the space is non-trivial is not enough.)
Continuous linear maps themselves form a seminormed space with respect to the operator norm.
Equations
- continuous_linear_map.to_semi_normed_group = semi_normed_group.of_core (E →L[𝕜] F) continuous_linear_map.to_semi_normed_group._proof_1
The operator norm is submultiplicative.
Continuous linear maps form a seminormed ring with respect to the operator norm.
Equations
- continuous_linear_map.to_semi_normed_ring = {to_has_norm := semi_normed_group.to_has_norm continuous_linear_map.to_semi_normed_group, to_ring := continuous_linear_map.ring normed_top_group, to_pseudo_metric_space := semi_normed_group.to_pseudo_metric_space continuous_linear_map.to_semi_normed_group, dist_eq := _, norm_mul := _}
continuous_linear_map.prod
as a linear_isometry_equiv
.
Equations
A continuous linear map is automatically uniformly continuous.
A continuous linear map is an isometry if and only if it preserves the norm.
If a continuous linear map is constructed from a linear map via the constructor mk_continuous
,
then its norm is bounded by the bound given to the constructor if it is nonnegative.
If a continuous linear map is constructed from a linear map via the constructor mk_continuous
,
then its norm is bounded by the bound or zero if bound is negative.
Create a bilinear map (represented as a map E →L[𝕜] F →L[𝕜] G
) from the corresponding linear
map and a bound on the norm of the image. The linear map can be constructed using
linear_map.mk₂
.
Equations
- f.mk_continuous₂ C hC = {to_fun := λ (x : E), (⇑f x).mk_continuous (C * ∥x∥) _, map_add' := _, map_smul' := _}.mk_continuous (max C 0) _
Flip the order of arguments of a continuous bilinear map.
For a version bundled as linear_isometry_equiv
, see
continuous_linear_map.flipL
.
Equations
- f.flip = (linear_map.mk₂ 𝕜 (λ (y : F) (x : E), ⇑(⇑f x) y) _ _ _ _).mk_continuous₂ ∥f∥ _
Flip the order of arguments of a continuous bilinear map.
This is a version bundled as a linear_isometry_equiv
.
For an unbundled version see continuous_linear_map.flip
.
Equations
- continuous_linear_map.flipₗᵢ 𝕜 E F G = {to_linear_equiv := {to_fun := continuous_linear_map.flip _inst_7, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.flip _inst_7, left_inv := _, right_inv := _}, norm_map' := _}
The continuous linear map obtained by applying a continuous linear map at a given vector.
This is the continuous version of linear_map.applyₗ
.
Equations
- continuous_linear_map.apply 𝕜 F = (continuous_linear_map.id 𝕜 (E →L[𝕜] F)).flip
Composition of continuous linear maps as a continuous bilinear map.
Equations
- continuous_linear_map.compL 𝕜 E F G = (linear_map.mk₂ 𝕜 continuous_linear_map.comp _ _ _ _).mk_continuous₂ 1 _
Left multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.
Equations
- continuous_linear_map.lmulₗᵢ 𝕜 𝕜' = {to_linear_map := ↑((algebra.lmul 𝕜 𝕜').to_linear_map.mk_continuous₂ 1 _), norm_map' := _}
Left multiplication in a normed algebra as a continuous bilinear map.
Equations
Right-multiplication in a normed algebra, considered as a continuous linear map.
Equations
Right-multiplication in a normed algebra, considered as a linear isometry to the space of continuous linear maps.
Equations
- continuous_linear_map.lmul_rightₗᵢ 𝕜 𝕜' = {to_linear_map := ↑(continuous_linear_map.lmul_right 𝕜 𝕜'), norm_map' := _}
Simultaneous left- and right-multiplication in a normed algebra, considered as a continuous trilinear map.
Equations
- continuous_linear_map.lmul_left_right 𝕜 𝕜' = ((continuous_linear_map.compL 𝕜 𝕜' 𝕜' 𝕜').comp (continuous_linear_map.lmul_right 𝕜 𝕜')).flip.comp (continuous_linear_map.lmul 𝕜 𝕜')
Scalar multiplication as a continuous bilinear map.
Equations
- continuous_linear_map.lsmul 𝕜 𝕜' = (algebra.lsmul 𝕜 E).to_linear_map.mk_continuous₂ 1 _
continuous_linear_map.restrict_scalars
as a linear_isometry
.
Equations
- continuous_linear_map.restrict_scalars_isometry 𝕜 E F 𝕜' 𝕜'' = {to_linear_map := continuous_linear_map.restrict_scalarsₗ 𝕜 E F 𝕜' 𝕜'' normed_top_group, norm_map' := _}
continuous_linear_map.restrict_scalars
as a continuous_linear_map
.
Equations
- continuous_linear_map.restrict_scalarsL 𝕜 E F 𝕜' 𝕜'' = (continuous_linear_map.restrict_scalars_isometry 𝕜 E F 𝕜' 𝕜'').to_continuous_linear_map
Applying a continuous linear map commutes with taking an (infinite) sum.
Alias of continuous_linear_map.has_sum
.
Alias of continuous_linear_map.summable
.
Applying a continuous linear map commutes with taking an (infinite) sum.
A linear equivalence which is a homothety is a continuous linear equivalence.
Equations
- continuous_linear_equiv.of_homothety f a ha hf = {to_linear_equiv := f, continuous_to_fun := _, continuous_inv_fun := _}
Construct a continuous linear equivalence from a linear equivalence together with bounds in both directions.
Equations
- e.to_continuous_linear_equiv_of_bounds C_to C_inv h_to h_inv = {to_linear_equiv := e, continuous_to_fun := _, continuous_inv_fun := _}
Compose a bilinear map E →L[𝕜] F →L[𝕜] G
with two linear maps E' →L[𝕜] E
and F' →L[𝕜] F
.
Derivative of a continuous bilinear map f : E →L[𝕜] F →L[𝕜] G
interpreted as a map E × F → G
at point p : E × F
evaluated at q : E × F
, as a continuous bilinear map.
Equations
- f.deriv₂ = f.bilinear_comp (continuous_linear_map.fst 𝕜 E F) (continuous_linear_map.snd 𝕜 E F) + f.flip.bilinear_comp (continuous_linear_map.snd 𝕜 E F) (continuous_linear_map.fst 𝕜 E F)
An operator is zero iff its norm vanishes.
If a normed space is non-trivial, then the norm of the identity equals 1
.
Continuous linear maps themselves form a normed space with respect to the operator norm.
Equations
- continuous_linear_map.to_normed_group = normed_group.of_core (E →L[𝕜] F) continuous_linear_map.to_normed_group._proof_2
Equations
- continuous_linear_map.to_normed_space = {to_semimodule := continuous_linear_map.semimodule continuous_linear_map.to_normed_space._proof_2, norm_smul_le := _}
Continuous linear maps form a normed ring with respect to the operator norm.
Equations
- continuous_linear_map.to_normed_ring = {to_has_norm := normed_group.to_has_norm continuous_linear_map.to_normed_group, to_ring := continuous_linear_map.ring continuous_linear_map.to_normed_ring._proof_1, to_metric_space := normed_group.to_metric_space continuous_linear_map.to_normed_group, dist_eq := _, norm_mul := _}
For a nonzero normed space E
, continuous linear endomorphisms form a normed algebra with
respect to the operator norm.
If a continuous linear map is a uniform embedding, then it is expands the distances by a positive factor.
If the target space is complete, the space of continuous linear maps with its norm is also complete. This works also if the source space is seminormed.
Extension of a continuous linear map f : E →L[𝕜] F
, with E
a normed space and F
a
complete normed space, along a uniform and dense embedding e : E →L[𝕜] G
.
If a dense embedding e : E →L[𝕜] G
expands the norm by a constant factor N⁻¹
, then the
norm of the extension of f
along e
is bounded by N * ∥f∥
.
Precomposition with a linear isometry preserves the operator norm.
The norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the norms.
continuous_linear_map.smul_right
as a continuous trilinear map:
smul_rightL (c : E →L[𝕜] 𝕜) (f : F) (x : E) = c x • f
.
Equations
- continuous_linear_map.smul_rightL 𝕜 E F = {to_fun := continuous_linear_map.smul_rightₗ _, map_add' := _, map_smul' := _}.mk_continuous₂ 1 _
A continuous linear equiv is a uniform embedding.
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
Given a nonzero element x
of a normed space E₁
over a field 𝕜
, the natural continuous
linear map from the span of x
to 𝕜
.