The topological dual of a normed space
In this file we define the topological dual of a normed space, and the bounded linear map from a normed space into its double dual.
We also prove that, for base field π
with [is_R_or_C π]
, this map is an isometry.
We then consider inner product spaces, with base field over β
(the corresponding results for β
will require the definition of conjugate-linear maps). We define to_dual_map
, a continuous linear
map from E
to its dual, which maps an element x
of the space to Ξ» y, βͺx, yβ«
. We check
(to_dual_map_isometry
) that this map is an isometry onto its image, and particular is injective.
We also define to_dual'
as the function taking taking a vector to its dual for a base field π
with [is_R_or_C π]
; this is a function and not a linear map.
Finally, under the hypothesis of completeness (i.e., for Hilbert spaces), we prove the FrΓ©chet-Riesz
representation (to_dual_map_eq_top
), which states the surjectivity: every element of the dual
of a Hilbert space E
has the form Ξ» u, βͺx, uβ«
for some x : E
. This permits the map
to_dual_map
to be upgraded to an (isometric) continuous linear equivalence, to_dual
, between a
Hilbert space and its dual.
References
- [M. Einsiedler and T. Ward, Functional Analysis, Spectral Theory, and Applications] [EinsiedlerWard2017]
Tags
dual, FrΓ©chet-Riesz
The topological dual of a normed space E
.
Equations
- normed_space.dual π E = (E βL[π] π)
Equations
- normed_space.dual.inhabited π E = {default := 0}
The inclusion of a normed space in its double (topological) dual.
Equations
- normed_space.inclusion_in_double_dual' π E x = {to_fun := Ξ» (f : normed_space.dual π E), βf x, map_add' := _, map_smul' := _}.mk_continuous β₯xβ₯ _
The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.
Equations
- normed_space.inclusion_in_double_dual π E = {to_fun := Ξ» (x : E), normed_space.inclusion_in_double_dual' π E x, map_add' := _, map_smul' := _}.mk_continuous 1 _
If one controls the norm of every f x
, then one controls the norm of x
.
Compare continuous_linear_map.op_norm_le_bound
.
The inclusion of a normed space in its double dual is an isometry onto its image.
Given some x
in an inner product space, we can define its dual as the continuous linear map
Ξ» y, βͺx, yβ«
. Consider using to_dual
or to_dual_map
instead in the real case.
In an inner product space, the norm of the dual of a vector x
is β₯xβ₯
FrΓ©chet-Riesz representation: any β
in the dual of a Hilbert space E
is of the form
Ξ» u, βͺy, uβ«
for some y : E
, i.e. to_dual'
is surjective.
In a real inner product space F
, the function that takes a vector x
in F
to its dual
Ξ» y, βͺx, yβ«
is a continuous linear map. If the space is complete (i.e. is a Hilbert space),
consider using to_dual
instead.
Equations
- inner_product_space.to_dual_map = {to_fun := β(inner_product_space.to_dual' β), map_add' := _, map_smul' := _}.mk_continuous 1 inner_product_space.to_dual_map._proof_3
In an inner product space, the norm of the dual of a vector x
is β₯xβ₯
FrΓ©chet-Riesz representation: any β
in the dual of a real Hilbert space F
is of the form
Ξ» u, βͺy, uβ«
for some y
in F
. See inner_product_space.to_dual
for the continuous linear
equivalence thus induced.
FrΓ©chet-Riesz representation: If F
is a Hilbert space, the function that takes a vector in F
to
its dual is a continuous linear equivalence.
FrΓ©chet-Riesz representation: If F
is a Hilbert space, the function that takes a vector in F
to
its dual is an isometry.
In a Hilbert space, the norm of a vector in the dual space is the norm of its corresponding primal vector.