Documentation

Mathlib.Analysis.Normed.Operator.WeakOperatorTopology

The weak operator topology #

This file defines a type copy of E →L[𝕜] F (where F is a normed space) which is endowed with the weak operator topology (WOT) rather than the topology induced by the operator norm. The WOT is defined as the coarsest topology such that the functional fun A => y (A x) is continuous for any x : E and y : NormedSpace.Dual 𝕜 F. Equivalently, a function f tends to A : E →WOT[𝕜] F along filter l iff y (f a x) tends to y (A x) along the same filter.

Basic non-topological properties of E →L[𝕜] F (such as the module structure) are copied over to the type copy.

We also prove that the WOT is induced by the family of seminorms ‖y (A x)‖ for x : E and y : NormedSpace.Dual 𝕜 F.

Main declarations #

Notation #

Implementation notes #

In the literature, the WOT is only defined on maps between Banach spaces. Here, we generalize this a bit to E →L[𝕜] F where F is an normed space, and E actually only needs to be a vector space with some topology for most results in this file.

@[irreducible]
def ContinuousLinearMapWOT (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [Semiring 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] :
Type (max u_2 u_3)

The type copy of E →L[𝕜] F endowed with the weak operator topology, denoted as E →WOT[𝕜] F.

Equations
Instances For

    The type copy of E →L[𝕜] F endowed with the weak operator topology, denoted as E →WOT[𝕜] F.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Basic properties common with E →L[𝕜] F #

      The section copies basic non-topological properties of E →L[𝕜] F over to E →WOT[𝕜] F, such as the module structure, FunLike, etc.

      instance ContinuousLinearMapWOT.instAddCommGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
      Equations
      instance ContinuousLinearMapWOT.instModule {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
      Module 𝕜 (E →WOT[𝕜]F)
      Equations
      def ContinuousLinearMap.toWOT (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
      (E →L[𝕜] F) ≃ₗ[𝕜] E →WOT[𝕜]F

      The linear equivalence that sends a continuous linear map to the type copy endowed with the weak operator topology.

      Equations
      Instances For
        instance ContinuousLinearMapWOT.instFunLike {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
        FunLike (E →WOT[𝕜]F) E F
        Equations
        Equations
        • =
        theorem ContinuousLinearMap.toWOT_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {A : E →L[𝕜] F} {x : E} :
        ((ContinuousLinearMap.toWOT 𝕜 E F) A) x = A x
        theorem ContinuousLinearMapWOT.ext {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {A : E →WOT[𝕜]F} {B : E →WOT[𝕜]F} (h : ∀ (x : E), A x = B x) :
        A = B
        theorem ContinuousLinearMapWOT.ext_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {A : E →WOT[𝕜]F} {B : E →WOT[𝕜]F} :
        A = B ∀ (x : E), A x = B x
        theorem ContinuousLinearMapWOT.ext_dual_iff {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {A : E →WOT[𝕜]F} {B : E →WOT[𝕜]F} :
        A = B ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)
        theorem ContinuousLinearMapWOT.ext_dual {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {A : E →WOT[𝕜]F} {B : E →WOT[𝕜]F} (h : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), y (A x) = y (B x)) :
        A = B
        @[simp]
        theorem ContinuousLinearMapWOT.zero_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) :
        0 x = 0
        @[simp]
        theorem ContinuousLinearMapWOT.add_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →WOT[𝕜]F} {g : E →WOT[𝕜]F} (x : E) :
        (f + g) x = f x + g x
        @[simp]
        theorem ContinuousLinearMapWOT.sub_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →WOT[𝕜]F} {g : E →WOT[𝕜]F} (x : E) :
        (f - g) x = f x - g x
        @[simp]
        theorem ContinuousLinearMapWOT.neg_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →WOT[𝕜]F} (x : E) :
        (-f) x = -f x
        @[simp]
        theorem ContinuousLinearMapWOT.smul_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E →WOT[𝕜]F} (c : 𝕜) (x : E) :
        (c f) x = c f x

        The topology of E →WOT[𝕜] F #

        The section endows E →WOT[𝕜] F with the weak operator topology and shows the basic properties of this topology. In particular, we show that it is a topological vector space.

        def ContinuousLinearMapWOT.inducingFn (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
        (E →WOT[𝕜]F) →ₗ[𝕜] E × NormedSpace.Dual 𝕜 F𝕜

        The function that induces the topology on E →WOT[𝕜] F, namely the function that takes an A and maps it to fun ⟨x, y⟩ => y (A x) in E × F⋆ → 𝕜, bundled as a linear map to make it easier to prove that it is a TVS.

        Equations
        Instances For
          instance ContinuousLinearMapWOT.instTopologicalSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :

          The weak operator topology is the coarsest topology such that fun A => y (A x) is continuous for all x, y.

          Equations
          theorem ContinuousLinearMapWOT.continuous_dual_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : NormedSpace.Dual 𝕜 F) :
          Continuous fun (A : E →WOT[𝕜]F) => y (A x)
          theorem ContinuousLinearMapWOT.continuous_of_dual_apply_continuous {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {α : Type u_4} [TopologicalSpace α] {g : αE →WOT[𝕜]F} (h : ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Continuous fun (a : α) => y ((g a) x)) :
          theorem ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {α : Type u_4} {l : Filter α} {f : αE →WOT[𝕜]F} {A : E →WOT[𝕜]F} :
          Filter.Tendsto f l (nhds A) ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Filter.Tendsto (fun (a : α) => y ((f a) x)) l (nhds (y (A x)))

          The defining property of the weak operator topology: a function f tends to A : E →WOT[𝕜] F along filter l iff y (f a x) tends to y (A x) along the same filter.

          theorem ContinuousLinearMapWOT.le_nhds_iff_forall_dual_apply_le_nhds {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {l : Filter (E →WOT[𝕜]F)} {A : E →WOT[𝕜]F} :
          l nhds A ∀ (x : E) (y : NormedSpace.Dual 𝕜 F), Filter.map (fun (T : E →WOT[𝕜]F) => y (T x)) l nhds (y (A x))
          instance ContinuousLinearMapWOT.instT3Space {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
          T3Space (E →WOT[𝕜]F)
          Equations
          • =
          instance ContinuousLinearMapWOT.instContinuousAdd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
          Equations
          • =
          instance ContinuousLinearMapWOT.instContinuousNeg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
          Equations
          • =
          instance ContinuousLinearMapWOT.instContinuousSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
          ContinuousSMul 𝕜 (E →WOT[𝕜]F)
          Equations
          • =
          Equations
          • =
          instance ContinuousLinearMapWOT.instUniformSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
          Equations
          instance ContinuousLinearMapWOT.instUniformAddGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
          Equations
          • =

          The WOT is induced by a family of seminorms #

          def ContinuousLinearMapWOT.seminorm {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (x : E) (y : NormedSpace.Dual 𝕜 F) :
          Seminorm 𝕜 (E →WOT[𝕜]F)

          The family of seminorms that induce the weak operator topology, namely ‖y (A x)‖ for all x and y.

          Equations
          Instances For
            def ContinuousLinearMapWOT.seminormFamily (𝕜 : Type u_1) (E : Type u_2) (F : Type u_3) [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
            SeminormFamily 𝕜 (E →WOT[𝕜]F) (E × NormedSpace.Dual 𝕜 F)

            The family of seminorms that induce the weak operator topology, namely ‖y (A x)‖ for all x and y.

            Equations
            Instances For
              theorem ContinuousLinearMapWOT.hasBasis_seminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
              (nhds 0).HasBasis (ContinuousLinearMapWOT.seminormFamily 𝕜 E F).basisSets id
              instance ContinuousLinearMapWOT.instLocallyConvexSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [Module (E →WOT[𝕜]F)] [IsScalarTower 𝕜 (E →WOT[𝕜]F)] :
              Equations
              • =
              theorem ContinuousLinearMap.continuous_toWOT {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :

              The weak operator topology is coarser than the norm topology, i.e. the inclusion map is continuous.

              def ContinuousLinearMap.toWOTCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
              (E →L[𝕜] F) →L[𝕜] E →WOT[𝕜]F

              The inclusion map from E →[𝕜] F to E →WOT[𝕜] F, bundled as a continuous linear map.

              Equations
              Instances For