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 StrongDual 𝕜 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 StrongDual 𝕜 E → WeakDual 𝕜 E is continuous, and as a consequence the weak-* topology is coarser than the topology obtained from the operator norm (dual norm).

The file also equips WeakDual 𝕜 E with the norm bornology inherited from StrongDual 𝕜 E, so that IsBounded refers to operator-norm boundedness. This is a pragmatic choice discussed further in the implementation notes.

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

The first main result concerns the comparison of the operator norm topology on StrongDual 𝕜 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.

Main definitions

• StrongDual.toWeakDual and WeakDual.toStrongDual: Linear equivalences between the dual types.
• WeakDual.instBornology: The norm bornology on WeakDual 𝕜 E.
• WeakDual.seminormFamily: The family of seminorms fun x f ↦ ‖f x‖ generating the weak-* topology.
• WeakDual.polar: The polar set of s : Set E viewed as a subset of WeakDual 𝕜 E.

Main results

Topology comparison

• NormedSpace.Dual.toWeakDual_continuous: The weak-* topology is coarser than the norm topology.

Bornology and pointwise bounds

• WeakDual.isBounded_iff_isVonNBounded: Equivalence of norm and weak-* boundedness for Banach spaces.

Compactness and Banach-Alaoglu

• WeakDual.isCompact_polar: Polars of neighborhoods of the origin are weak-* compact.
• WeakDual.isCompact_closedBall: Closed balls are weak-* compact.
• WeakDual.isSeqCompact_closedBall: Sequential version for separable spaces.

Implementation notes

• Topology synonym: When M is a vector space, the duals StrongDual 𝕜 M and WeakDual 𝕜 M are type synonyms with different topology instances.
• Bornology choice: The Bornology instance on WeakDual 𝕜 E is inherited from StrongDual 𝕜 E via inferInstanceAs and corresponds to the operator-norm bornology. While the natural bornology for a weak topology is technically the von Neumann bornology (pointwise boundedness), we use the norm bornology for several pragmatic reasons:
  1. Practicality: In the normed setting, "bounded" is almost universally synonymous with "norm-bounded". This allows IsBounded to be used directly in statements like Banach-Alaoglu.
  2. Clarity: It preserves a clear distinction between norm-boundedness (IsBounded) and topological weak-* boundedness (IsVonNBounded).
  3. Consistency: By the Uniform Boundedness Principle, these notions coincide whenever E is a Banach space (isBounded_iff_isVonNBounded).
• Polar sets: The polar set polar 𝕜 s of a subset s of E is originally defined as a subset of the dual StrongDual 𝕜 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).
• Banach-Alaoglu Proof: The weak dual of E is embedded in the space of functions E → 𝕜 with the topology of pointwise convergence.

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.

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

Equivalences between StrongDual and WeakDual

def StrongDual.toWeakDual {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] : StrongDual R M ≃ₗ[R] WeakDual R M

For vector spaces M, there is a canonical map StrongDual R M → WeakDual R M (the "identity" mapping). It is a linear equivalence.

Equations

• StrongDual.toWeakDual = LinearEquiv.refl R (StrongDual R M)

@[deprecated StrongDual.toWeakDual (since := "2025-08-03")]

def NormedSpace.Dual.toWeakDual {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] : StrongDual R M ≃ₗ[R] WeakDual R M

Alias of StrongDual.toWeakDual.

---

For vector spaces M, there is a canonical map StrongDual R M → WeakDual R M (the "identity" mapping). It is a linear equivalence.

Equations

• @NormedSpace.Dual.toWeakDual = @StrongDual.toWeakDual

theorem StrongDual.coe_toWeakDual {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] (x' : StrongDual R M) : ⇑(toWeakDual x') = ⇑x'

@[simp]

theorem StrongDual.toWeakDual_apply {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] (x' : StrongDual R M) (y : M) : (toWeakDual x') y = x' y

@[deprecated StrongDual.coe_toWeakDual (since := "2025-08-03")]

theorem NormedSpace.Dual.coe_toWeakDual {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] (x' : StrongDual R M) : ⇑(StrongDual.toWeakDual x') = ⇑x'

Alias of StrongDual.coe_toWeakDual.

theorem StrongDual.toWeakDual_inj {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] (x' y' : StrongDual R M) : toWeakDual x' = toWeakDual y' ↔ x' = y'

@[deprecated StrongDual.toWeakDual_inj (since := "2025-08-03")]

theorem NormedSpace.Dual.toWeakDual_inj {R : Type u_1} [CommSemiring R] [TopologicalSpace R] [ContinuousAdd R] [ContinuousConstSMul R R] {M : Type u_2} [AddCommMonoid M] [TopologicalSpace M] [Module R M] (x' y' : StrongDual R M) : StrongDual.toWeakDual x' = StrongDual.toWeakDual y' ↔ x' = y'

Alias of StrongDual.toWeakDual_inj.

noncomputable def WeakDual.toStrongDual {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] : WeakDual 𝕜 E ≃ₗ[𝕜] StrongDual 𝕜 E

For vector spaces E, there is a canonical map WeakDual 𝕜 E → StrongDual 𝕜 E (the "identity" mapping). It is a linear equivalence. Here it is implemented as the inverse of the linear equivalence StrongDual.toWeakDual in the other direction.

Equations

• WeakDual.toStrongDual = StrongDual.toWeakDual.symm

@[simp]

theorem WeakDual.toStrongDual_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (x : WeakDual 𝕜 E) (y : E) : (toStrongDual x) y = x y

theorem WeakDual.coe_toStrongDual {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (x' : WeakDual 𝕜 E) : ⇑(toStrongDual x') = ⇑x'

theorem WeakDual.toStrongDual_inj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [AddCommMonoid E] [TopologicalSpace E] [Module 𝕜 E] (x' y' : WeakDual 𝕜 E) : toStrongDual x' = toStrongDual y' ↔ x' = y'

@[implicit_reducible]

instance WeakDual.instBornology {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Bornology (WeakDual 𝕜 E)

The bornology on WeakDual 𝕜 F is the norm bornology inherited from StrongDual 𝕜 F.

Note: This is a pragmatic choice. To be precise, the bornology of a weak topology should be the von Neumann bornology (pointwise boundedness). However, in the normed setting, IsBounded is most useful when referring to the operator norm (e.g., to state Banach-Alaoglu concisely).

Pointwise boundedness is instead captured by Bornology.IsVonNBounded. For Banach spaces, these notions coincide via isBounded_iff_isVonNBounded. See the module docstring for more details.

Equations

• WeakDual.instBornology = { cobounded := WeakDual.instBornology._aux_1, le_cofinite := ⋯ }

@[simp]

theorem WeakDual.isBounded_toStrongDual_preimage_iff_isBounded {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set (StrongDual 𝕜 E)} : Bornology.IsBounded (⇑toStrongDual ⁻¹' s) ↔ Bornology.IsBounded s

A set in WeakDual 𝕜 E is bounded iff its image in StrongDual 𝕜 E is bounded.

@[simp]

theorem WeakDual.isBounded_toWeakDual_preimage_iff_isBounded {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_3} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)} : Bornology.IsBounded (⇑StrongDual.toWeakDual ⁻¹' s) ↔ Bornology.IsBounded s

A set in StrongDual 𝕜 E is bounded iff its image in WeakDual 𝕜 E is bounded.

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

theorem NormedSpace.Dual.toWeakDual_continuous {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Continuous fun (x' : StrongDual 𝕜 E) => StrongDual.toWeakDual x'

def NormedSpace.Dual.continuousLinearMapToWeakDual {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : StrongDual 𝕜 E →L[𝕜] WeakDual 𝕜 E

For a normed space E, according to toWeakDual_continuous the "identity mapping" StrongDual 𝕜 E → WeakDual 𝕜 E is continuous. This definition implements it as a continuous linear map.

Equations

• NormedSpace.Dual.continuousLinearMapToWeakDual = { toLinearMap := ↑StrongDual.toWeakDual, cont := ⋯ }

theorem NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : ContinuousLinearMap.uniformSpace.toTopologicalSpace ≤ instTopologicalSpaceWeakDual 𝕜 E

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

Bornology and pointwise bounds

This section relates the inherited norm bornology (IsBounded) to the intrinsic von Neumann bornology of the weak-* topology (IsVonNBounded).

The following results justify using the norm bornology as the default instance: by the Uniform Boundedness Principle, it coincides with the von Neumann bornology whenever $E$ is a Banach space.

def WeakDual.seminormFamily (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : SeminormFamily 𝕜 (WeakDual 𝕜 E) E

The family of seminorms on WeakDual 𝕜 E given by fun x f ↦ ‖f x‖, indexed by E. This is the seminorm family associated to the weak-* topology via topDualPairing.

Equations

• WeakDual.seminormFamily 𝕜 E = (topDualPairing 𝕜 E).toSeminormFamily

@[simp]

theorem WeakDual.seminormFamily_apply {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x : E) (f : WeakDual 𝕜 E) : (seminormFamily 𝕜 E x) f = ‖f x‖

theorem WeakDual.withSeminorms (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] (E : Type u_2) [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : WithSeminorms (seminormFamily 𝕜 E)

theorem WeakDual.isBounded_iff_isVonNBounded {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] {s : Set (WeakDual 𝕜 E)} : Bornology.IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s

By the Uniform Boundedness Principle, norm-boundedness (the default bornology) and pointwise-boundedness (IsVonNBounded) coincide on the weak dual of a Banach space.

Compactness of bounded closed sets

While the coercion ↑ : WeakDual 𝕜 E → (E → 𝕜) is not a closed map, it sends bounded closed sets to closed sets.

theorem WeakDual.isClosed_image_coe_of_bounded_of_closed {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set (WeakDual 𝕜 E)} (hb : Bornology.IsBounded s) (hc : IsClosed s) : IsClosed (DFunLike.coe '' s)

The coercion ↑ : WeakDual 𝕜 E → (E → 𝕜) sends bounded closed sets to closed sets.

theorem WeakDual.isCompact_of_bounded_of_closed {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 E)} (hb : Bornology.IsBounded s) (hc : IsClosed s) : IsCompact s

Bounded closed sets in WeakDual 𝕜 E are compact when 𝕜 is a proper space.

Closed balls

theorem WeakDual.isClosed_closedBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x' : StrongDual 𝕜 E) (r : ℝ) : IsClosed (⇑toStrongDual ⁻¹' Metric.closedBall x' r)

Closed balls in StrongDual 𝕜 E pull back to closed sets in WeakDual 𝕜 E.

theorem WeakDual.isBounded_closedBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (x' : StrongDual 𝕜 E) (r : ℝ) : Bornology.IsBounded (⇑toStrongDual ⁻¹' Metric.closedBall x' r)

Closed balls are bounded in the weak dual.

theorem WeakDual.isCompact_closedBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] (x' : StrongDual 𝕜 E) (r : ℝ) : IsCompact (⇑toStrongDual ⁻¹' Metric.closedBall x' r)

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

Polar sets in the weak dual space

def WeakDual.polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [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

• WeakDual.polar 𝕜 s = ⇑WeakDual.toStrongDual ⁻¹' StrongDual.polar 𝕜 s

theorem WeakDual.polar_def (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : polar 𝕜 s = {f : WeakDual 𝕜 E | ∀ x ∈ s, ‖f x‖ ≤ 1}

theorem WeakDual.isClosed_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : IsClosed (polar 𝕜 s)

The polar polar 𝕜 s of a set s : E is a closed subset when the weak star topology is used.

theorem WeakDual.isBounded_polar (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (s_nhds : s ∈ nhds 0) : Bornology.IsBounded (polar 𝕜 s)

Polar sets of neighborhoods of the origin are bounded in the weak dual.

theorem WeakDual.isClosed_image_polar_of_mem_nhds (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (s_nhds : s ∈ nhds 0) : IsClosed (DFunLike.coe '' 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) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} (s_nhds : s ∈ nhds 0) : IsClosed (DFunLike.coe '' StrongDual.polar 𝕜 s)

The image under ↑ : StrongDual 𝕜 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) [NontriviallyNormedField 𝕜] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] [ProperSpace 𝕜] {s : Set E} (s_nhds : s ∈ nhds 0) : IsCompact (polar 𝕜 s)

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.

Sequential compactness

theorem WeakDual.exists_countable_separating (𝕜 : Type u_3) (V : Type u_4) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [TopologicalSpace.SeparableSpace V] : ∃ (gs : ℕ → WeakDual 𝕜 V → 𝕜), (∀ (n : ℕ), Continuous (gs n)) ∧ ∀ ⦃x y : WeakDual 𝕜 V⦄, x ≠ y → ∃ (n : ℕ), gs n x ≠ gs n y

In a separable normed space, there exists a sequence of continuous functions that separates points of the weak dual.

theorem WeakDual.metrizable_of_isCompact (𝕜 : Type u_3) (V : Type u_4) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [TopologicalSpace.SeparableSpace V] (K : Set (WeakDual 𝕜 V)) (K_cpt : IsCompact K) : TopologicalSpace.MetrizableSpace ↑K

A compact subset of the weak dual of a separable normed space is metrizable.

theorem WeakDual.isSeqCompact_of_isBounded_of_isClosed (𝕜 : Type u_3) (V : Type u_4) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [TopologicalSpace.SeparableSpace V] [ProperSpace 𝕜] {s : Set (WeakDual 𝕜 V)} (hb : Bornology.IsBounded s) (hc : IsClosed s) : IsSeqCompact s

Bounded closed sets in the weak dual of a separable normed space are sequentially compact.

theorem WeakDual.isSeqCompact_polar (𝕜 : Type u_3) (V : Type u_4) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [TopologicalSpace.SeparableSpace V] [ProperSpace 𝕜] {s : Set V} (s_nhd : s ∈ nhds 0) : IsSeqCompact (polar 𝕜 s)

The Sequential Banach-Alaoglu theorem: the polar set of a neighborhood s of the origin in a separable normed space V is a sequentially compact subset of WeakDual 𝕜 V.

theorem WeakDual.isSeqCompact_closedBall (𝕜 : Type u_3) (V : Type u_4) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup V] [NormedSpace 𝕜 V] [TopologicalSpace.SeparableSpace V] [ProperSpace 𝕜] (x' : StrongDual 𝕜 V) (r : ℝ) : IsSeqCompact (⇑toStrongDual ⁻¹' Metric.closedBall x' r)

The Sequential Banach-Alaoglu theorem: closed balls of the dual of a separable normed space V are sequentially compact in the weak-* topology.