Operator norm on the space of continuous linear maps #
Define the operator norm on the space of continuous (semi)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 seminormed_add_comm_group
and we specialize to normed_add_comm_group
at the end.
Note that most of statements that apply to semilinear maps only hold when the ring homomorphism
is isometric, as expressed by the typeclass [ring_hom_isometric σ]
.
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 nontrivially
normed. The continuity ensures boundedness on a ball of some radius ε
. The nontriviality of the
norm 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 𝕜
to E
by taking multiples of x
.
Equations
Given a unit-length element x
of a normed space E
over a field 𝕜
, the natural linear
isometry map from 𝕜
to E
by taking multiples of x
.
Equations
- linear_isometry.to_span_singleton 𝕜 E hv = {to_linear_map := {to_fun := (linear_map.to_span_singleton 𝕜 E v).to_fun, map_add' := _, map_smul' := _}, norm_map' := _}
The operator norm of a continuous linear map is the inf of all its bounds.
Equations
If one controls the norm of every A x
, then one controls the norm of A
.
If one controls the norm of every A x
, ∥x∥ ≠ 0
, then one controls the norm of A
.
The fundamental property of the operator norm: ∥f x∥ ≤ ∥f∥ * ∥x∥
.
The image of the unit ball under a continuous linear map is bounded.
For a continuous real linear map f
, if one controls the norm of every f x
, ∥x∥ = 1
, then
one controls the norm of f
.
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_seminormed_add_comm_group = seminormed_add_comm_group.of_core (E →SL[σ₁₂] F) continuous_linear_map.to_seminormed_add_comm_group._proof_1
If one controls the norm of every A x
, then one controls the norm of A
.
If one controls the norm of every A x
, ∥x∥₊ ≠ 0
, then one controls the norm of A
.
For a continuous real linear map f
, if one controls the norm of every f x
, ∥x∥₊ = 1
, then
one controls the norm of f
.
Equations
- continuous_linear_map.to_normed_space = {to_module := continuous_linear_map.module continuous_linear_map.to_normed_space._proof_2, norm_smul_le := _}
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 := seminormed_add_comm_group.to_has_norm continuous_linear_map.to_seminormed_add_comm_group, to_ring := {add := add_comm_group.add seminormed_add_comm_group.to_add_comm_group, add_assoc := _, zero := add_comm_group.zero seminormed_add_comm_group.to_add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul seminormed_add_comm_group.to_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg seminormed_add_comm_group.to_add_comm_group, sub := add_comm_group.sub seminormed_add_comm_group.to_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul seminormed_add_comm_group.to_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast continuous_linear_map.ring, nat_cast := ring.nat_cast continuous_linear_map.ring, one := ring.one continuous_linear_map.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul continuous_linear_map.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow continuous_linear_map.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}, to_pseudo_metric_space := seminormed_add_comm_group.to_pseudo_metric_space continuous_linear_map.to_seminormed_add_comm_group, dist_eq := _, norm_mul := _}
For a normed space E
, continuous linear endomorphisms form a normed algebra with
respect to the operator norm.
continuous linear maps are Lipschitz continuous.
Evaluation of a continuous linear map f
at a point is Lipschitz continuous in f
.
continuous_linear_map.prod
as a linear_isometry_equiv
.
Equations
- continuous_linear_map.prodₗᵢ R = {to_linear_equiv := continuous_linear_map.prodₗ R continuous_linear_map.prodₗᵢ._proof_22, norm_map' := _}
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 (linear_order.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_18, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.flip _inst_17, left_inv := _, right_inv := _}, norm_map' := _}
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 _, map_add' := _, map_smul' := _, inv_fun := continuous_linear_map.flip _, left_inv := _, right_inv := _}, norm_map' := _}
The continuous semilinear map obtained by applying a continuous semilinear 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 →SL[σ₁₂] F)).flip
The continuous semilinear map obtained by applying a continuous semilinear 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 semilinear maps as a continuous semibilinear map.
Equations
- continuous_linear_map.compSL E F G σ₁₂ σ₂₃ = (linear_map.mk₂'ₛₗ (ring_hom.id 𝕜₃) σ₂₃ continuous_linear_map.comp _ _ _ _).mk_continuous₂ 1 _
Composition of continuous linear maps as a continuous bilinear map.
Equations
- continuous_linear_map.compL 𝕜 E Fₗ Gₗ = continuous_linear_map.compSL E Fₗ Gₗ (ring_hom.id 𝕜) (ring_hom.id 𝕜)
Apply L(x,-)
pointwise to bilinear maps, as a continuous bilinear map
Equations
- continuous_linear_map.precompR Eₗ L = (continuous_linear_map.compL 𝕜 Eₗ Fₗ Gₗ).comp L
Apply L(-,y)
pointwise to bilinear maps, as a continuous bilinear map
Equations
continuous_linear_map.prod_map
as a continuous linear map.
Equations
- continuous_linear_map.prod_mapL 𝕜 M₁ M₂ M₃ M₄ = (have Φ₁ : (M₁ →L[𝕜] M₂) →L[𝕜] M₁ →L[𝕜] M₂ × M₄, from ⇑(continuous_linear_map.compL 𝕜 M₁ M₂ (M₂ × M₄)) (continuous_linear_map.inl 𝕜 M₂ M₄), have Φ₂ : (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₂ × M₄, from ⇑(continuous_linear_map.compL 𝕜 M₃ M₄ (M₂ × M₄)) (continuous_linear_map.inr 𝕜 M₂ M₄), have Φ₁' : (M₁ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄, from ⇑((continuous_linear_map.compL 𝕜 (M₁ × M₃) M₁ (M₂ × M₄)).flip) (continuous_linear_map.fst 𝕜 M₁ M₃), have Φ₂' : (M₃ →L[𝕜] M₂ × M₄) →L[𝕜] M₁ × M₃ →L[𝕜] M₂ × M₄, from ⇑((continuous_linear_map.compL 𝕜 (M₁ × M₃) M₃ (M₂ × M₄)).flip) (continuous_linear_map.snd 𝕜 M₁ M₃), have Ψ₁ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₁ →L[𝕜] M₂, from continuous_linear_map.fst 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄), have Ψ₂ : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄) →L[𝕜] M₃ →L[𝕜] M₄, from continuous_linear_map.snd 𝕜 (M₁ →L[𝕜] M₂) (M₃ →L[𝕜] M₄), Φ₁'.comp (Φ₁.comp Ψ₁) + Φ₂'.comp (Φ₂.comp Ψ₂)).copy (λ (p : (M₁ →L[𝕜] M₂) × (M₃ →L[𝕜] M₄)), p.fst.prod_map p.snd) _
Left multiplication in a normed algebra as a continuous bilinear map.
Equations
- continuous_linear_map.lmul 𝕜 𝕜' = (linear_map.mul 𝕜 𝕜').mk_continuous₂ 1 _
Right-multiplication in a normed algebra, considered as a continuous linear map.
Equations
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 𝕜 𝕜')
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 := ↑(continuous_linear_map.lmul 𝕜 𝕜'), norm_map' := _}
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' := _}
Scalar multiplication as a continuous bilinear map.
Equations
- continuous_linear_map.lsmul 𝕜 𝕜' = (algebra.lsmul 𝕜 E).to_linear_map.mk_continuous₂ 1 _
The norm of lsmul
is at most 1 in any semi-normed group.
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.
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 →SL[σ₁₃] F →SL[σ₂₃] G
with two linear maps
E' →SL[σ₁'] E
and F' →SL[σ₂'] 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ₗ)
linear_map.bound_of_ball_bound'
is a version of this lemma over a field satisfying is_R_or_C
that produces a concrete bound.
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_add_comm_group = normed_add_comm_group.of_core (E →SL[σ₁₂] F) continuous_linear_map.to_normed_add_comm_group._proof_2
Continuous linear maps form a normed ring with respect to the operator norm.
Equations
- continuous_linear_map.to_normed_ring = {to_has_norm := normed_add_comm_group.to_has_norm continuous_linear_map.to_normed_add_comm_group, to_ring := semi_normed_ring.to_ring continuous_linear_map.to_semi_normed_ring, to_metric_space := normed_add_comm_group.to_metric_space continuous_linear_map.to_normed_add_comm_group, dist_eq := _, norm_mul := _}
If a continuous linear map is a uniform embedding, then it is expands the distances by a positive factor.
Construct a bundled continuous (semi)linear map from a map f : E → F
and a proof of the fact
that it belongs to the closure of the image of a bounded set s : set (E →SL[σ₁₂] F)
under coercion
to function. Coercion to function of the result is definitionally equal to f
.
Let f : E → F
be a map, let g : α → E →SL[σ₁₂] F
be a family of continuous (semi)linear maps
that takes values in a bounded set and converges to f
pointwise along a nontrivial filter. Then
f
is a continuous (semi)linear map.
Equations
If a Cauchy sequence of continuous linear map converges to a continuous linear map pointwise, then it converges to the same map in norm. This lemma is used to prove that the space of continuous linear maps is complete provided that the codomain is a complete space.
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.
Let s
be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F
taking values
in a proper space. Then s
interpreted as a set in the space of maps E → F
with topology of
pointwise convergence is precompact: its closure is a compact set.
Let s
be a bounded set in the space of continuous (semi)linear maps E →SL[σ] F
taking values
in a proper space. If s
interpreted as a set in the space of maps E → F
with topology of
pointwise convergence is closed, then it is compact.
TODO: reformulate this in terms of a type synonym with the right topology.
If a set s
of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions E → F
is a closed set. We don't have a name for E →SL[σ] F
with weak-* topology in mathlib
, so we use an equivalent condition (see is_closed_induced_iff'
).
TODO: reformulate this in terms of a type synonym with the right topology.
If a set s
of semilinear functions is bounded and is closed in the weak-* topology, then its
image under coercion to functions E → F
is a compact set. We don't have a name for E →SL[σ] F
with weak-* topology in mathlib
, so we use an equivalent condition (see is_closed_induced_iff'
).
A closed ball is closed in the weak-* topology. We don't have a name for E →SL[σ] F
with
weak-* topology in mathlib
, so we use an equivalent condition (see is_closed_induced_iff'
).
The set of functions f : E → F
that represent continuous linear maps f : E →SL[σ₁₂] F
at distance ≤ r
from f₀ : E →SL[σ₁₂] F
is closed in the topology of pointwise convergence.
This is one of the key steps in the proof of the Banach-Alaoglu theorem.
Banach-Alaoglu theorem. The set of functions f : E → F
that represent continuous linear
maps f : E →SL[σ₁₂] F
at distance ≤ r
from f₀ : E →SL[σ₁₂] F
is compact in the topology of
pointwise convergence. Other versions of this theorem can be found in
analysis.normed_space.weak_dual
.
Extension of a continuous linear map f : E →SL[σ₁₂] F
, with E
a normed space and F
a
complete normed space, along a uniform and dense embedding e : E →L[𝕜] Fₗ
.
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∥
.
Postcomposition of a continuous linear map with a linear isometry preserves the operator norm.
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.
The non-negative norm of the tensor product of a scalar linear map and of an element of a normed space is the product of the non-negative 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 _
The norm of lsmul
equals 1 in any nontrivial normed group.
This is continuous_linear_map.op_norm_lsmul_le
as an equality.
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 𝕜
.
Equations
A pair of continuous (semi)linear equivalences generates an continuous (semi)linear equivalence between the spaces of continuous (semi)linear maps.
A pair of continuous linear equivalences generates an continuous linear equivalence between the spaces of continuous linear maps.
Equations
- e₁.arrow_congr e₂ = e₁.arrow_congrSL e₂
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
.