The topological dual of a normed space #
In this file we define the topological dual NormedSpace.Dual
of a normed space, and the
continuous linear map NormedSpace.inclusionInDoubleDual
from a normed space into its double
dual.
For base field ๐ = โ
or ๐ = โ
, this map is actually an isometric embedding; we provide a
version NormedSpace.inclusionInDoubleDualLi
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 SeminormedAddCommGroup
and we specialize to NormedAddCommGroup
when needed.
Main definitions #
inclusionInDoubleDual
andinclusionInDoubleDualLi
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
.
References #
Tags #
dual, polar
The topological dual of a seminormed space E
.
Equations
- NormedSpace.Dual ๐ E = (E โL[๐] ๐)
Instances For
Equations
- NormedSpace.instDual ๐ E = inferInstance
Equations
- NormedSpace.instSeminormedAddCommGroupDual ๐ E = inferInstance
The inclusion of a normed space in its double (topological) dual, considered as a bounded linear map.
Equations
- NormedSpace.inclusionInDoubleDual ๐ E = ContinuousLinearMap.apply ๐ ๐
Instances For
The dual pairing as a bilinear form.
Equations
- NormedSpace.dualPairing ๐ E = ContinuousLinearMap.coeLM ๐
Instances For
If one controls the norm of every f x
, then one controls the norm of x
.
Compare ContinuousLinearMap.opNorm_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
- NormedSpace.inclusionInDoubleDualLi ๐ = let __src := NormedSpace.inclusionInDoubleDual ๐ E; { toLinearMap := โ__src, norm_map' := โฏ }
Instances For
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
- NormedSpace.polar ๐ = (NormedSpace.dualPairing ๐ E).flip.polar
Instances For
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.