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 σ]
.
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.
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. This is only a temporary definition because we want to replace the topology
with continuous_linear_map.topological_space
to avoid diamond issues.
See Note [forgetful inheritance]
Equations
The pseudo_metric_space
structure on E →SL[σ₁₂] F
coming from
continuous_linear_map.tmp_seminormed_add_comm_group
.
See Note [forgetful inheritance]
The uniform_space
structure on E →SL[σ₁₂] F
coming from
continuous_linear_map.tmp_seminormed_add_comm_group
.
See Note [forgetful inheritance]
The topological_space
structure on E →SL[σ₁₂] F
coming from
continuous_linear_map.tmp_seminormed_add_comm_group
.
See Note [forgetful inheritance]
Equations
- continuous_linear_map.to_pseudo_metric_space = continuous_linear_map.tmp_pseudo_metric_space.replace_uniformity continuous_linear_map.to_pseudo_metric_space._proof_1
Continuous linear maps themselves form a seminormed space with respect to the operator norm.
Equations
- continuous_linear_map.to_seminormed_add_comm_group = {to_has_norm := seminormed_add_comm_group.to_has_norm continuous_linear_map.tmp_seminormed_add_comm_group, to_add_comm_group := continuous_linear_map.add_comm_group seminormed_add_comm_group.to_topological_add_group, to_pseudo_metric_space := continuous_linear_map.to_pseudo_metric_space _inst_17, dist_eq := _}
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) _
Multiplication in a non-unital normed algebra as a continuous bilinear map.
Equations
- continuous_linear_map.mul 𝕜 𝕜' = (linear_map.mul 𝕜 𝕜').mk_continuous₂ 1 _
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 linear_map.mul_left_right
,
but there is a minor difference: linear_map.mul_left_right
is uncurried.
Equations
- continuous_linear_map.mul_left_right 𝕜 𝕜' = ((continuous_linear_map.compL 𝕜 𝕜' 𝕜' 𝕜').comp (continuous_linear_map.mul 𝕜 𝕜').flip).flip.comp (continuous_linear_map.mul 𝕜 𝕜')
Multiplication in a normed algebra as a linear isometry to the space of continuous linear maps.
Equations
- continuous_linear_map.mulₗᵢ 𝕜 𝕜' = {to_linear_map := ↑(continuous_linear_map.mul 𝕜 𝕜'), 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ₗ 𝕜' 𝕜'' seminormed_add_comm_group.to_topological_add_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
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_separation continuous_linear_map.to_normed_add_comm_group._proof_1
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 := _}