mathlib documentation

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.

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:

TODOs:

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.

References #

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

noncomputable def normed_space.dual.to_weak_dual {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] :
normed_space.dual ๐•œ E โ‰ƒโ‚—[๐•œ] weak_dual ๐•œ E

For normed spaces E, there is a canonical map dual ๐•œ E โ†’ weak_dual ๐•œ E (the "identity" mapping). It is a linear equivalence.

Equations
noncomputable def weak_dual.to_normed_dual {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] :
weak_dual ๐•œ E โ‰ƒโ‚—[๐•œ] normed_space.dual ๐•œ 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} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] (x' : normed_space.dual ๐•œ E) :
@[simp]
theorem normed_space.dual.to_weak_dual_eq_iff {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] (x' y' : normed_space.dual ๐•œ E) :
@[simp]
theorem weak_dual.to_normed_dual_eq_iff {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] (x' y' : weak_dual ๐•œ E) :
theorem normed_space.dual.to_weak_dual_continuous {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] :
noncomputable def normed_space.dual.continuous_linear_map_to_weak_dual {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] :
normed_space.dual ๐•œ E โ†’L[๐•œ] weak_dual ๐•œ 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

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

def weak_dual.polar (๐•œ : Type u_1) [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] (s : set E) :
set (weak_dual ๐•œ 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 weak_dual.polar ๐•œ s.

Equations
theorem weak_dual.is_closed_polar {๐•œ : Type u_1} [nondiscrete_normed_field ๐•œ] {E : Type u_2} [normed_group E] [normed_space ๐•œ E] (s : set E) :

The polar polar ๐•œ s of a set s : E is a closed subset when the weak star topology is used, i.e., when polar ๐•œ s is interpreted as a subset of weak_dual ๐•œ E.