The topological dual of a normed space #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file we define the topological dual
normed_space.dual of a normed space, and the
continuous linear map
normed_space.inclusion_in_double_dual from a normed space into its double
For base field
𝕜 = ℝ or
𝕜 = ℂ, this map is actually an isometric embedding; we provide a
normed_space.inclusion_in_double_dual_li of the map which is of type a bundled linear
E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E)).
Since a lot of elementary properties don't require
eq_of_dist_eq_zero we start setting up the
seminormed_add_comm_group and we specialize to
normed_add_comm_group when needed.
Main definitions #
inclusion_in_double_dual_liare 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 topological dual of a seminormed space
- normed_space.dual 𝕜 E = (E →L[𝕜] 𝕜)
The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.
The dual pairing as a bilinear form.
If one controls the norm of every
f x, then one controls the norm of
The inclusion of a normed space in its double dual is an isometry onto its image.
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.