# 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
`NormedSpace.Dual ๐ 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 `NormedSpace.Dual ๐ 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 `Dual ๐ E โ WeakDual ๐ E`

.

`NormedSpace.Dual.toWeakDual`

and`WeakDual.toNormedDual`

: Linear equivalences from`dual ๐ E`

to`WeakDual ๐ E`

and in the converse direction.`NormedSpace.Dual.continuousLinearMapToWeakDual`

: A continuous linear mapping from`Dual ๐ E`

to`WeakDual ๐ E`

(same as`NormedSpace.Dual.toWeakDual`

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) `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 `E`

is a normed space, the duals `Dual ๐ E`

and `WeakDual ๐ 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 `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

### 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 โ WeakDual ๐ 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 โ WeakDual ๐ E`

(the "identity"
mapping). It is a linear equivalence.

## Equations

- NormedSpace.Dual.toWeakDual = LinearEquiv.refl ๐ (E โL[๐] ๐)

## Instances For

For a normed space `E`

, according to `toWeakDual_continuous`

the "identity mapping"
`Dual ๐ E โ WeakDual ๐ E`

is continuous. This definition implements it as a continuous linear
map.

## Equations

- NormedSpace.Dual.continuousLinearMapToWeakDual = { toLinearMap := โNormedSpace.Dual.toWeakDual, cont := โฏ }

## Instances For

The weak-star topology is coarser than the dual-norm topology.

For normed spaces `E`

, there is a canonical map `WeakDual ๐ E โ Dual ๐ E`

(the "identity"
mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear
equivalence `NormedSpace.Dual.toWeakDual`

in the other direction.

## Equations

- WeakDual.toNormedDual = NormedSpace.Dual.toWeakDual.symm

## Instances For

### 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 `WeakDual.polar ๐ s`

.

## Equations

- WeakDual.polar ๐ s = โWeakDual.toNormedDual โปยน' NormedSpace.polar ๐ s

## Instances For

The polar `polar ๐ s`

of a set `s : E`

is a closed subset when the weak star topology
is used.

While the coercion `โ : WeakDual ๐ E โ (E โ ๐)`

is not a closed map, it sends *bounded*
closed sets to closed sets.

The image under `โ : WeakDual ๐ E โ (E โ ๐)`

of a polar `WeakDual.polar ๐ s`

of a
neighborhood `s`

of the origin is a closed set.

The image under `โ : NormedSpace.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 `WeakDual ๐ E`

.

The **Banach-Alaoglu theorem**: closed balls of the dual of a normed space `E`

are compact in
the weak-star topology.