Documentation

Mathlib.Analysis.Normed.Module.WeakDual

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.

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:

TODO #

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 #

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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (x' : NormedSpace.Dual ๐•œ E) :
    NormedSpace.Dual.toWeakDual x' = x'
    @[simp]
    theorem NormedSpace.Dual.toWeakDual_eq_iff {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
    Continuous fun (x' : NormedSpace.Dual ๐•œ E) => NormedSpace.Dual.toWeakDual x'
    def NormedSpace.Dual.continuousLinearMapToWeakDual {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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 = { toLinearMap := โ†‘NormedSpace.Dual.toWeakDual, cont := โ‹ฏ }
    Instances For
      theorem NormedSpace.Dual.dual_norm_topology_le_weak_dual_topology {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] :
      UniformSpace.toTopologicalSpace โ‰ค WeakDual.instTopologicalSpace

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

      def WeakDual.toNormedDual {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (x : WeakDual ๐•œ E) (y : E) :
        (WeakDual.toNormedDual x) y = x y
        @[simp]
        theorem WeakDual.coe_toNormedDual {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (x' : WeakDual ๐•œ E) :
        WeakDual.toNormedDual x' = x'
        @[simp]
        theorem WeakDual.toNormedDual_eq_iff {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (x' : WeakDual ๐•œ E) (y' : WeakDual ๐•œ E) :
        WeakDual.toNormedDual x' = WeakDual.toNormedDual y' โ†” x' = y'
        theorem WeakDual.isClosed_closedBall {๐•œ : Type u_1} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (x' : NormedSpace.Dual ๐•œ E) (r : โ„) :
        IsClosed (โ‡‘WeakDual.toNormedDual โปยน' Metric.closedBall x' r)

        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
        Instances For
          theorem WeakDual.polar_def (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (s : Set E) :
          WeakDual.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 (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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] {s : Set (WeakDual ๐•œ E)} (hb : Bornology.IsBounded (โ‡‘NormedSpace.Dual.toWeakDual โปยน' s)) (hc : IsClosed s) :
          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} [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] [ProperSpace ๐•œ] {s : Set (WeakDual ๐•œ E)} (hb : Bornology.IsBounded (โ‡‘NormedSpace.Dual.toWeakDual โปยน' s)) (hc : IsClosed s) :
          theorem WeakDual.isClosed_image_polar_of_mem_nhds (๐•œ : Type u_1) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [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) [NontriviallyNormedField ๐•œ] {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] [ProperSpace ๐•œ] (x' : NormedSpace.Dual ๐•œ E) (r : โ„) :
          IsCompact (โ‡‘WeakDual.toNormedDual โปยน' 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.