# mathlibdocumentation

analysis.normed_space.weak_dual

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

The file is a stub, some TODOs below.

## Main definitions #

The main definitions concern the canonical mapping dual 𝕜 E → weak_dual 𝕜 E.

• normed_space.dual.to_weak_dual and weak_dual.to_normed_dual: Linear equivalences from dual 𝕜 E to weak_dual 𝕜 E and in the converse direction.
• normed_space.dual.continuous_linear_map_to_weak_dual: A continuous linear mapping from dual 𝕜 E to weak_dual 𝕜 E (same as normed_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.

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 Banach-Alaoglu theorem (general version maybe in topology.algebra.weak_dual_topology).
• Add metrizability of the dual unit ball (more generally bounded subsets) of weak_dual 𝕜 E under the assumption of separability of E. Sequential Banach-Alaoglu theorem would then follow from the general one.

## Notations #

No new notation is introduced.

## Implementation notes #

Weak-* topology is defined generally in the file topology.algebra.weak_dual_topology.

When E is a normed space, the duals dual 𝕜 E and weak_dual 𝕜 E are type synonyms with different topology instances.

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

def normed_space.dual.to_weak_dual {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :
≃ₗ[𝕜] E

For normed spaces E, there is a canonical map dual 𝕜 E → weak_dual 𝕜 E (the "identity" mapping). It is a linear equivalence.

Equations
def weak_dual.to_normed_dual {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :
E ≃ₗ[𝕜]

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.

Equations
@[simp]
theorem weak_dual.coe_to_fun_eq_normed_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (x' : E) :
@[simp]
theorem normed_space.dual.to_weak_dual_eq_iff {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (x' y' : E) :
@[simp]
theorem weak_dual.to_normed_dual_eq_iff {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] (x' y' : E) :
x' = y'
theorem normed_space.dual.to_weak_dual_continuous {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :
continuous (λ (x' : ,
def normed_space.dual.continuous_linear_map_to_weak_dual {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :
→L[𝕜] E

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
theorem normed_space.dual.dual_norm_topology_le_weak_dual_topology {𝕜 : Type u_1} {E : Type u_2} [normed_group E] [ E] :

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