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 StrongDual 𝕜 E or WeakDual 𝕜 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 StrongDual 𝕜 E → WeakDual 𝕜 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 StrongDual 𝕜 E → WeakDual 𝕜 E.

StrongDual.toWeakDual and WeakDual.toStrongDual: Linear equivalences from StrongDual 𝕜 E to WeakDual 𝕜 E and in the converse direction.
NormedSpace.Dual.continuousLinearMapToWeakDual: A continuous linear mapping from StrongDual 𝕜 E to WeakDual 𝕜 E (same as StrongDual.toWeakDual but different bundled data).

Main results #

The first main result concerns the comparison of the operator norm topology on StrongDual 𝕜 E and the weak-* topology on (its type synonym) WeakDual 𝕜 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.
WeakDual.isCompact_polar (a version of the Banach-Alaoglu theorem): The polar set of a neighborhood of the origin in a normed space E over 𝕜 is compact in WeakDual _ E, if the nontrivially normed field 𝕜 is proper as a topological space.
WeakDual.isCompact_closedBall (the most common special case of the Banach-Alaoglu theorem): Closed balls in the dual of a normed space E over ℝ or ℂ are compact in the weak-star topology.

TODO #

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 WeakDual 𝕜 E under the assumption of separability of E.
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.WeakDual.

When M is a vector space, the duals StrongDual 𝕜 M and WeakDual 𝕜 M 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 StrongDual 𝕜 E. We care about properties of these w.r.t. weak-* topology, and for this purpose give the definition WeakDual.polar 𝕜 s for the "same" subset viewed as a subset of WeakDual 𝕜 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