The topological dual of a normed space #
For base field
𝕜 = ℝ or
𝕜 = ℂ, this map is actually an isometric embedding; we provide a
NormedSpace.inclusionInDoubleDualLi of the map which is of type a bundled linear
E →ₗᵢ[𝕜] (Dual 𝕜 (Dual 𝕜 E)).
Main definitions #
inclusionInDoubleDualLiare the inclusion of a normed space in its double dual, considered as a bounded linear map and as a linear isometry, respectively.
polar 𝕜 sis the subset of
Dual 𝕜 Econsisting of those functionals
‖x' z‖ ≤ 1for every
z ∈ s.
The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.
If one controls the norm of every
f x, then one controls the norm of
Given a subset
s in a normed space
E (over a field
𝕜), the polar
polar 𝕜 s is the subset of
Dual 𝕜 E consisting of those functionals which
evaluate to something of norm at most one at all points
z ∈ s.
x' is a dual element such that the norms
‖x' z‖ are bounded for
z ∈ s, then a
small scalar multiple of
x' is in
polar 𝕜 s.
polar of closed ball in a normed space
E is the closed ball of the dual with
Given a neighborhood
s of the origin in a normed space
E, the dual norms
of all elements of the polar
polar 𝕜 s are bounded by a constant.