The topological dual of a normed space #
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
dual.
For base field π = β
or π = β
, this map is actually an isometric embedding; we provide a
version normed_space.inclusion_in_double_dual_li
of the map which is of type a bundled linear
isometric embedding, E ββα΅’[π] (dual π (dual π E))
.
Since a lot of elementary properties don't require eq_of_dist_eq_zero
we start setting up the
theory for seminormed_add_comm_group
and we specialize to normed_add_comm_group
when needed.
Main definitions #
inclusion_in_double_dual
andinclusion_in_double_dual_li
are the inclusion of a normed space in its double dual, considered as a bounded linear map and as a linear isometry, respectively.polar π s
is the subset ofdual π E
consisting of those functionalsx'
for whichβx' zβ β€ 1
for everyz β s
.
Tags #
dual
The topological dual of a seminormed space E
.
Equations
- normed_space.dual π E = (E βL[π] π)
Equations
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 = continuous_linear_map.apply π π
The dual pairing as a bilinear form.
Equations
- normed_space.dual_pairing π E = continuous_linear_map.coe_lm π
If one controls the norm of every f x
, then one controls the norm of x
.
Compare continuous_linear_map.op_norm_le_bound
.
See also geometric_hahn_banach_point_point
.
The inclusion of a normed space in its double dual is an isometry onto its image.
Equations
- normed_space.inclusion_in_double_dual_li π = {to_linear_map := (normed_space.inclusion_in_double_dual π E).to_linear_map, norm_map' := _}
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
.
Equations
- normed_space.polar π = (normed_space.dual_pairing π E).flip.polar
If 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
.
The polar
of closed ball in a normed space E
is the closed ball of the dual with
inverse radius.
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.