# 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.

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 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).

def NormedSpace.Dual.toWeakDual {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] :
NormedSpace.Dual ๐ E โโ[๐] WeakDual ๐ E

For normed spaces E, there is a canonical map Dual ๐ E โ WeakDual ๐ E (the "identity" mapping). It is a linear equivalence.

Equations
Instances For
@[simp]
theorem NormedSpace.Dual.coe_toWeakDual {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (x' : NormedSpace.Dual ๐ E) :
NormedSpace.Dual.toWeakDual x' = x'
@[simp]
theorem NormedSpace.Dual.toWeakDual_eq_iff {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (x' : NormedSpace.Dual ๐ E) (y' : NormedSpace.Dual ๐ E) :
NormedSpace.Dual.toWeakDual x' = NormedSpace.Dual.toWeakDual y' โ x' = y'
theorem NormedSpace.Dual.toWeakDual_continuous {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] :
Continuous fun (x' : NormedSpace.Dual ๐ E) => NormedSpace.Dual.toWeakDual x'
def NormedSpace.Dual.continuousLinearMapToWeakDual {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] :
NormedSpace.Dual ๐ E โL[๐] WeakDual ๐ E

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 = let __src := NormedSpace.Dual.toWeakDual; { toLinearMap := โ__src, cont := โฏ }
Instances For
theorem NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] :
UniformSpace.toTopologicalSpace โค WeakDual.instTopologicalSpace

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

def WeakDual.toNormedDual {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] :
WeakDual ๐ E โโ[๐] NormedSpace.Dual ๐ E

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
theorem WeakDual.toNormedDual_apply {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (x : WeakDual ๐ E) (y : E) :
(WeakDual.toNormedDual x) y = x y
@[simp]
theorem WeakDual.coe_toNormedDual {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (x' : WeakDual ๐ E) :
WeakDual.toNormedDual x' = x'
@[simp]
theorem WeakDual.toNormedDual_eq_iff {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (x' : WeakDual ๐ E) (y' : WeakDual ๐ E) :
WeakDual.toNormedDual x' = WeakDual.toNormedDual y' โ x' = y'
theorem WeakDual.isClosed_closedBall {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] (x' : NormedSpace.Dual ๐ E) (r : โ) :
IsClosed (โWeakDual.toNormedDual โปยน' )

### Polar sets in the weak dual space #

def WeakDual.polar (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] (s : Set E) :
Set (WeakDual ๐ E)

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
Instances For
theorem WeakDual.polar_def (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] (s : Set E) :
WeakDual.polar ๐ s = {f : WeakDual ๐ E | โ x โ s, โf xโ โค 1}
theorem WeakDual.isClosed_polar (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] (s : Set E) :
IsClosed (WeakDual.polar ๐ s)

The polar polar ๐ s of a set s : E is a closed subset when the weak star topology is used.

theorem WeakDual.isClosed_image_coe_of_bounded_of_closed {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] {s : Set (WeakDual ๐ E)} (hb : Bornology.IsBounded (โNormedSpace.Dual.toWeakDual โปยน' s)) (hc : ) :
IsClosed (DFunLike.coe '' s)

While the coercion โ : WeakDual ๐ E โ (E โ ๐) is not a closed map, it sends bounded closed sets to closed sets.

theorem WeakDual.isCompact_of_bounded_of_closed {๐ : Type u_1} [] {E : Type u_2} [NormedSpace ๐ E] [ProperSpace ๐] {s : Set (WeakDual ๐ E)} (hb : Bornology.IsBounded (โNormedSpace.Dual.toWeakDual โปยน' s)) (hc : ) :
theorem WeakDual.isClosed_image_polar_of_mem_nhds (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] {s : Set E} (s_nhd : s โ nhds 0) :
IsClosed (DFunLike.coe '' WeakDual.polar ๐ s)

The image under โ : WeakDual ๐ E โ (E โ ๐) of a polar WeakDual.polar ๐ s of a neighborhood s of the origin is a closed set.

theorem NormedSpace.Dual.isClosed_image_polar_of_mem_nhds (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] {s : Set E} (s_nhd : s โ nhds 0) :
IsClosed (DFunLike.coe '' NormedSpace.polar ๐ s)

The image under โ : NormedSpace.Dual ๐ E โ (E โ ๐) of a polar polar ๐ s of a neighborhood s of the origin is a closed set.

theorem WeakDual.isCompact_polar (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] [ProperSpace ๐] {s : Set E} (s_nhd : s โ nhds 0) :

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.

theorem WeakDual.isCompact_closedBall (๐ : Type u_1) [] {E : Type u_2} [NormedSpace ๐ E] [ProperSpace ๐] (x' : NormedSpace.Dual ๐ E) (r : โ) :
IsCompact (โWeakDual.toNormedDual โปยน' )

The Banach-Alaoglu theorem: closed balls of the dual of a normed space E are compact in the weak-star topology.