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

• ContinuousLinearMapWOT 𝕜 E F: The type copy of E →L[𝕜] F endowed with the weak operator topology.
• ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto: 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.
• ContinuousLinearMap.toWOT: the inclusion map from E →L[𝕜] F to the type copy
• ContinuousLinearMap.continuous_toWOT: the inclusion map is continuous, i.e. the WOT is coarser than the norm topology.
• ContinuousLinearMapWOT.withSeminorms: the WOT is induced by the family of seminorms ‖y (A x)‖ for x : E and y : NormedSpace.Dual 𝕜 F.

Notation

• The type copy of E →L[𝕜] F endowed with the weak operator topology is denoted by E →WOT[𝕜] F.
• We locally use the notation F⋆ for NormedSpace.Dual 𝕜 F.

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

• (E →WOT[𝕜]F) = (E →L[𝕜] F)

def «term_→WOT[_]_» : Lean.TrailingParserDescr

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.

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] : AddCommGroup (E →WOT[𝕜]F)

Equations

• ContinuousLinearMapWOT.instAddCommGroup = inferInstanceAs (AddCommGroup (E →L[𝕜] F))

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

• ContinuousLinearMapWOT.instModule = inferInstanceAs (Module 𝕜 (E →L[𝕜] F))

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

• ContinuousLinearMap.toWOT 𝕜 E F = LinearEquiv.refl 𝕜 (E →L[𝕜] F)

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

• ContinuousLinearMapWOT.instFunLike = { coe := fun (f : E →WOT[𝕜]F) => ⇑((ContinuousLinearMap.toWOT 𝕜 E F).symm f), coe_injective' := ⋯ }

instance ContinuousLinearMapWOT.instContinuousLinearMapClass {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : ContinuousLinearMapClass (E →WOT[𝕜]F) 𝕜 E F

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 {𝕜 : 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

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)

@[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

• ContinuousLinearMapWOT.inducingFn 𝕜 E F = { toFun := fun (A : E →WOT[𝕜]F) (x : E × NormedSpace.Dual 𝕜 F) => match x with | (x, y) => y (A x), map_add' := ⋯, map_smul' := ⋯ }

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] : TopologicalSpace (E →WOT[𝕜]F)

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

Equations

• ContinuousLinearMapWOT.instTopologicalSpace = TopologicalSpace.induced (⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)) Pi.topologicalSpace

theorem ContinuousLinearMapWOT.continuous_inducingFn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : Continuous ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)

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)) : Continuous g

theorem ContinuousLinearMapWOT.embedding_inducingFn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : Embedding ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)

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] : ContinuousAdd (E →WOT[𝕜]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] : ContinuousNeg (E →WOT[𝕜]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

• ⋯ = ⋯

instance ContinuousLinearMapWOT.instTopologicalAddGroup {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : TopologicalAddGroup (E →WOT[𝕜]F)

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] : UniformSpace (E →WOT[𝕜]F)

Equations

• ContinuousLinearMapWOT.instUniformSpace = UniformSpace.comap (⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)) inferInstance

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] : UniformAddGroup (E →WOT[𝕜]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

• ContinuousLinearMapWOT.seminorm x y = { toFun := fun (A : E →WOT[𝕜]F) => ‖y (A x)‖, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯ }

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

• ContinuousLinearMapWOT.seminormFamily 𝕜 E F x = match x with | (x, y) => ContinuousLinearMapWOT.seminorm x y

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

theorem ContinuousLinearMapWOT.withSeminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] : WithSeminorms (ContinuousLinearMapWOT.seminormFamily 𝕜 E F)

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)] : LocallyConvexSpace ℝ (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] : Continuous ⇑(ContinuousLinearMap.toWOT 𝕜 E 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

• ContinuousLinearMap.toWOTCLM = { toLinearMap := ↑(ContinuousLinearMap.toWOT 𝕜 E F), cont := ⋯ }