Weak dual of normed space #
Let E
be a normed space over a field ๐
. This file is concerned with properties of the weak-*
topology on the dual of E
. By the dual, we mean either of the type synonyms
normed_space.dual ๐ E
or weak_dual ๐ E
, depending on whether it is viewed as equipped with its
usual operator norm topology or the weak-* topology.
It is shown that the canonical mapping normed_space.dual ๐ E โ weak_dual ๐ E
is continuous, and
as a consequence the weak-* topology is coarser than the topology obtained from the operator norm
(dual norm).
In this file, we also establish the Banach-Alaoglu theorem about the compactness of closed balls
in the dual of E
(as well as sets of somewhat more general form) with respect to the weak-*
topology.
Main definitions #
The main definitions concern the canonical mapping dual ๐ E โ weak_dual ๐ E
.
normed_space.dual.to_weak_dual
andweak_dual.to_normed_dual
: Linear equivalences fromdual ๐ E
toweak_dual ๐ E
and in the converse direction.normed_space.dual.continuous_linear_map_to_weak_dual
: A continuous linear mapping fromdual ๐ E
toweak_dual ๐ E
(same asnormed_space.dual.to_weak_dual
but different bundled data).
Main results #
The first main result concerns the comparison of the operator norm topology on dual ๐ E
and the
weak-* topology on (its type synonym) weak_dual ๐ E
:
dual_norm_topology_le_weak_dual_topology
: The weak-* topology on the dual of a normed space is coarser (not necessarily strictly) than the operator norm topology.weak_dual.is_compact_polar
(a version of the Banach-Alaoglu theorem): The polar set of a neighborhood of the origin in a normed spaceE
over๐
is compact inweak_dual _ E
, if the nontrivially normed field๐
is proper as a topological space.weak_dual.is_compact_closed_ball
(the most common special case of the Banach-Alaoglu theorem): Closed balls in the dual of a normed spaceE
overโ
orโ
are compact in the weak-star topology.
TODOs:
- Add that in finite dimensions, the weak-* topology and the dual norm topology coincide.
- Add that in infinite dimensions, the weak-* topology is strictly coarser than the dual norm topology.
- Add metrizability of the dual unit ball (more generally weak-star compact subsets) of
weak_dual ๐ E
under the assumption of separability ofE
. - Add the sequential Banach-Alaoglu theorem: the dual unit ball of a separable normed space
E
is sequentially compact in the weak-star topology. This would follow from the metrizability above.
Notations #
No new notation is introduced.
Implementation notes #
Weak-* topology is defined generally in the file topology.algebra.module.weak_dual
.
When E
is a normed space, the duals dual ๐ E
and weak_dual ๐ E
are type synonyms with
different topology instances.
For the proof of Banach-Alaoglu theorem, the weak dual of E
is embedded in the space of
functions E โ ๐
with the topology of pointwise convergence.
The polar set polar ๐ s
of a subset s
of E
is originally defined as a subset of the dual
dual ๐ E
. We care about properties of these w.r.t. weak-* topology, and for this purpose give
the definition weak_dual.polar ๐ s
for the "same" subset viewed as a subset of weak_dual ๐ E
(a type synonym of the dual but with a different topology instance).
References #
- https://en.wikipedia.org/wiki/Weak_topology#Weak-*_topology
- https://en.wikipedia.org/wiki/Banach%E2%80%93Alaoglu_theorem
Tags #
weak-star, weak dual
Weak star topology on duals of normed spaces #
In this section, we prove properties about the weak-* topology on duals of normed spaces.
We prove in particular that the canonical mapping dual ๐ E โ weak_dual ๐ E
is continuous,
i.e., that the weak-* topology is coarser (not necessarily strictly) than the topology given
by the dual-norm (i.e. the operator-norm).
For normed spaces E
, there is a canonical map dual ๐ E โ weak_dual ๐ E
(the "identity"
mapping). It is a linear equivalence.
Equations
- normed_space.dual.to_weak_dual = linear_equiv.refl ๐ (E โL[๐] ๐)
For a normed space E
, according to to_weak_dual_continuous
the "identity mapping"
dual ๐ E โ weak_dual ๐ E
is continuous. This definition implements it as a continuous linear
map.
Equations
- normed_space.dual.continuous_linear_map_to_weak_dual = {to_linear_map := {to_fun := normed_space.dual.to_weak_dual.to_fun, map_add' := _, map_smul' := _}, cont := _}
The weak-star topology is coarser than the dual-norm topology.
For normed spaces E
, there is a canonical map weak_dual ๐ E โ dual ๐ E
(the "identity"
mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
equivalence normed_space.dual.to_weak_dual
in the other direction.
Polar sets in the weak dual space #
The polar set polar ๐ s
of s : set E
seen as a subset of the dual of E
with the
weak-star topology is weak_dual.polar ๐ s
.
Equations
- weak_dual.polar ๐ s = โweak_dual.to_normed_dual โปยน' normed_space.polar ๐ s
The polar polar ๐ s
of a set s : E
is a closed subset when the weak star topology
is used.
While the coercion coe_fn : weak_dual ๐ E โ (E โ ๐)
is not a closed map, it sends bounded
closed sets to closed sets.
The image under coe_fn : weak_dual ๐ E โ (E โ ๐)
of a polar weak_dual.polar ๐ s
of a
neighborhood s
of the origin is a closed set.
The image under coe_fn : normed_space.dual ๐ E โ (E โ ๐)
of a polar polar ๐ s
of a
neighborhood s
of the origin is a closed set.
The Banach-Alaoglu theorem: the polar set of a neighborhood s
of the origin in a
normed space E
is a compact subset of weak_dual ๐ E
.
The Banach-Alaoglu theorem: closed balls of the dual of a normed space E
are compact in
the weak-star topology.