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 such as the real or the complex numbers, this map is an isometry.
More generically, this is proved for any field in the class has_exists_extension_norm_eq, i.e.,
satisfying the Hahn-Banach theorem.
The topological dual of a normed space E.
Equations
- normed_space.dual 𝕜 E = (E →L[𝕜] 𝕜)
Equations
- normed_space.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 real normed space in its double dual is an isometry onto its image.