mathlib3 documentation

analysis.normed_space.weak_dual

Weak dual of normed space #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

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 β†’ 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.

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 weak_dual.polar π•œ s for the "same" subset viewed as a subset of weak_dual π•œ E (a type synonym of the dual but with a different topology instance).

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} [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_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 normed_space.dual.continuous_linear_map_to_weak_dual {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_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.

noncomputable def weak_dual.to_normed_dual {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_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
theorem weak_dual.to_normed_dual_apply {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space π•œ E] (x : weak_dual π•œ E) (y : E) :
@[simp]
theorem weak_dual.coe_to_normed_dual {π•œ : Type u_1} [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space π•œ E] (x' : weak_dual π•œ E) :

Polar sets in the weak dual space #

def weak_dual.polar (π•œ : Type u_1) [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_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.polar_def (π•œ : Type u_1) [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space π•œ E] (s : set E) :
weak_dual.polar π•œ s = {f : weak_dual π•œ E | βˆ€ (x : E), x ∈ s β†’ ‖⇑f xβ€– ≀ 1}
theorem weak_dual.is_closed_polar (π•œ : Type u_1) [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_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.

While the coercion coe_fn : weak_dual π•œ E β†’ (E β†’ π•œ) is not a closed map, it sends bounded closed sets to closed sets.

theorem weak_dual.is_closed_image_polar_of_mem_nhds (π•œ : Type u_1) [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space π•œ E] {s : set E} (s_nhd : s ∈ nhds 0) :

The image under coe_fn : weak_dual π•œ E β†’ (E β†’ π•œ) of a polar weak_dual.polar π•œ s of a neighborhood s of the origin is a closed set.

theorem normed_space.dual.is_closed_image_polar_of_mem_nhds (π•œ : Type u_1) [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space π•œ E] {s : set E} (s_nhd : s ∈ nhds 0) :

The image under coe_fn : normed_space.dual π•œ E β†’ (E β†’ π•œ) of a polar polar π•œ s of a neighborhood s of the origin is a closed set.

theorem weak_dual.is_compact_polar (π•œ : Type u_1) [nontrivially_normed_field π•œ] {E : Type u_2} [seminormed_add_comm_group E] [normed_space π•œ E] [proper_space π•œ] {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 weak_dual π•œ E.

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