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.
Since a lot of elementary properties don't require eq_of_dist_eq_zero we start setting up the
theory for semi_normed_space and we specialize to normed_space when needed.
References #
Tags #
dual, FrΓ©chet-Riesz
The topological dual of a seminormed space E.
Equations
- normed_space.dual π E = (E βL[π] π)
Equations
- normed_space.dual.inhabited π E = {default := 0}
Equations
Equations
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.