Documentation

Mathlib.Topology.Algebra.Module.WeakDual

Weak dual topology #

We continue in the setting of Mathlib.Topology.Algebra.Module.WeakBilin, which defines the weak topology given two vector spaces E and F over a commutative semiring 𝕜 and a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜. The weak topology on E is the coarsest topology such that for all y : F every map fun x => B x y is continuous.

In this file, we consider two special cases. In the case that F = E →L[𝕜] 𝕜 and B being the canonical pairing, we obtain the weak-* topology, WeakDual 𝕜 E := (E →L[𝕜] 𝕜). Interchanging the arguments in the bilinear form yields the weak topology WeakSpace 𝕜 E := E.

Main definitions #

The main definitions are the types WeakDual 𝕜 E and WeakSpace 𝕜 E, with the respective topology instances on it.

Notations #

No new notation is introduced.

References #

Tags #

weak-star, weak dual, duality

def topDualPairing (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 𝕜] :
(E →L[𝕜] 𝕜) →ₗ[𝕜] E →ₗ[𝕜] 𝕜

The canonical pairing of a vector space and its topological dual.

Equations
Instances For
    theorem topDualPairing_apply {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousConstSMul 𝕜 𝕜] (v : E →L[𝕜] 𝕜) (x : E) :
    ((topDualPairing 𝕜 E) v) x = v x
    def WeakDual (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
    Type (max u_6 u_7)

    The weak star topology is the topology coarsest topology on E →L[𝕜] 𝕜 such that all functionals fun v => v x are continuous.

    Equations
    Instances For
      instance WeakDual.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Equations
      instance WeakDual.instModule {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Module 𝕜 (WeakDual 𝕜 E)
      Equations
      Equations
      instance WeakDual.instContinuousAdd {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Equations
      • =
      instance WeakDual.instInhabited {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Equations
      • WeakDual.instInhabited = ContinuousLinearMap.inhabited
      instance WeakDual.instFunLike {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      FunLike (WeakDual 𝕜 E) E 𝕜
      Equations
      • WeakDual.instFunLike = ContinuousLinearMap.funLike
      instance WeakDual.instContinuousLinearMapClass {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      ContinuousLinearMapClass (WeakDual 𝕜 E) 𝕜 E 𝕜
      Equations
      • =
      instance WeakDual.instCoeFunForall {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      CoeFun (WeakDual 𝕜 E) fun (x : WeakDual 𝕜 E) => E𝕜

      Helper instance for when there's too many metavariables to apply DFunLike.hasCoeToFun directly.

      Equations
      • WeakDual.instCoeFunForall = DFunLike.hasCoeToFun
      instance WeakDual.instMulAction {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :
      MulAction M (WeakDual 𝕜 E)

      If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it acts on WeakDual 𝕜 E.

      Equations
      instance WeakDual.instDistribMulAction {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :

      If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it acts distributively on WeakDual 𝕜 E.

      Equations
      instance WeakDual.instModule' {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (R : Type u_6) [Semiring R] [Module R 𝕜] [SMulCommClass 𝕜 R 𝕜] [ContinuousConstSMul R 𝕜] :
      Module R (WeakDual 𝕜 E)

      If 𝕜 is a topological module over a semiring R and scalar multiplication commutes with the multiplication on 𝕜, then WeakDual 𝕜 E is a module over R.

      Equations
      instance WeakDual.instContinuousConstSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [ContinuousConstSMul M 𝕜] :
      Equations
      • =
      instance WeakDual.instContinuousSMul {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (M : Type u_6) [Monoid M] [DistribMulAction M 𝕜] [SMulCommClass 𝕜 M 𝕜] [TopologicalSpace M] [ContinuousSMul M 𝕜] :

      If a monoid M distributively continuously acts on 𝕜 and this action commutes with multiplication on 𝕜, then it continuously acts on WeakDual 𝕜 E.

      Equations
      • =
      theorem WeakDual.coeFn_continuous {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Continuous fun (x : WeakDual 𝕜 E) (y : E) => x y
      theorem WeakDual.eval_continuous {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (y : E) :
      Continuous fun (x : WeakDual 𝕜 E) => x y
      theorem WeakDual.continuous_of_continuous_eval {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalSpace α] {g : αWeakDual 𝕜 E} (h : ∀ (y : E), Continuous fun (a : α) => (g a) y) :
      instance WeakDual.instT2Space {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [T2Space 𝕜] :
      T2Space (WeakDual 𝕜 E)
      Equations
      • =
      instance WeakDual.instAddCommGroup {𝕜 : Type u_2} {E : Type u_4} [CommRing 𝕜] [TopologicalSpace 𝕜] [TopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] :
      Equations
      Equations
      • =
      def WeakSpace (𝕜 : Type u_6) (E : Type u_7) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
      Type u_7

      The weak topology is the topology coarsest topology on E such that all functionals fun x => v x are continuous.

      Equations
      Instances For
        instance WeakSpace.instAddCommMonoid {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Equations
        instance WeakSpace.instModule {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Module 𝕜 (WeakSpace 𝕜 E)
        Equations
        Equations
        instance WeakSpace.instContinuousAdd {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
        Equations
        • =
        instance WeakSpace.instModule' {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [CommSemiring 𝕝] [Module 𝕝 E] :
        Module 𝕝 (WeakSpace 𝕜 E)
        Equations
        instance WeakSpace.instIsScalarTower {𝕜 : Type u_2} {𝕝 : Type u_3} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [CommSemiring 𝕝] [Module 𝕝 𝕜] [Module 𝕝 E] [IsScalarTower 𝕝 𝕜 E] :
        IsScalarTower 𝕝 𝕜 (WeakSpace 𝕜 E)
        Equations
        • =
        def WeakSpace.map {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) :
        WeakSpace 𝕜 E →L[𝕜] WeakSpace 𝕜 F

        A continuous linear map from E to F is still continuous when E and F are equipped with their weak topologies.

        Equations
        Instances For
          theorem WeakSpace.map_apply {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) (x : E) :
          (WeakSpace.map f) x = f x
          @[simp]
          theorem WeakSpace.coe_map {𝕜 : Type u_2} {E : Type u_4} {F : Type u_5} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] [AddCommMonoid F] [Module 𝕜 F] [TopologicalSpace F] (f : E →L[𝕜] F) :
          (WeakSpace.map f) = f
          def toWeakSpace (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
          E ≃ₗ[𝕜] WeakSpace 𝕜 E

          There is a canonical map E → WeakSpace 𝕜 E (the "identity" mapping). It is a linear equivalence.

          Equations
          Instances For
            def toWeakSpaceCLM (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
            E →L[𝕜] WeakSpace 𝕜 E

            For a topological vector space E, "identity mapping" E → WeakSpace 𝕜 E is continuous. This definition implements it as a continuous linear map.

            Equations
            Instances For
              @[simp]
              theorem toWeakSpaceCLM_eq_toWeakSpace (𝕜 : Type u_2) (E : Type u_4) [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (x : E) :
              (toWeakSpaceCLM 𝕜 E) x = (toWeakSpace 𝕜 E) x
              theorem isOpenMap_toWeakSpace_symm {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] :
              IsOpenMap (toWeakSpace 𝕜 E).symm

              The canonical map from WeakSpace 𝕜 E to E is an open map.

              theorem WeakSpace.isOpen_of_isOpen {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] (V : Set E) (hV : IsOpen ((toWeakSpaceCLM 𝕜 E) '' V)) :

              A set in E which is open in the weak topology is open.

              theorem tendsto_iff_forall_eval_tendsto_topDualPairing {α : Type u_1} {𝕜 : Type u_2} {E : Type u_4} [CommSemiring 𝕜] [TopologicalSpace 𝕜] [ContinuousAdd 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommMonoid E] [Module 𝕜 E] [TopologicalSpace E] {l : Filter α} {f : αWeakDual 𝕜 E} {x : WeakDual 𝕜 E} :
              Filter.Tendsto f l (nhds x) ∀ (y : E), Filter.Tendsto (fun (i : α) => ((topDualPairing 𝕜 E) (f i)) y) l (nhds (((topDualPairing 𝕜 E) x) y))
              instance WeakSpace.instAddCommGroup {𝕜 : Type u_2} {E : Type u_4} [CommRing 𝕜] [TopologicalSpace 𝕜] [TopologicalAddGroup 𝕜] [ContinuousConstSMul 𝕜 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] :
              Equations
              Equations
              • =