The weak operator topology

This file defines a type copy of E →L[𝕜] F (where E and F are topological vector spaces) which is endowed with the weak operator topology (WOT) rather than the topology of bounded convergence (which is the usual one induced by the operator norm in the normed setting). 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 : F →L[𝕜] 𝕜. 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 : F →L[𝕜] 𝕜.

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 : F →L[𝕜] 𝕜.

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 F →L[𝕜] 𝕜.

Implementation notes

In most of the literature, the WOT is defined on maps between Banach spaces. Here, we only assume that the domain and codomains are topological vector spaces over a normed field.

@[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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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) [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : ContinuousLinearMapClass (E →WOT[𝕜] F) 𝕜 E F

Equations

• ⋯ = ⋯

theorem ContinuousLinearMap.toWOT_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [H : SeparatingDual 𝕜 F] {A : E →WOT[𝕜] F} {B : E →WOT[𝕜] F} (h : ∀ (x : E) (y : F →L[𝕜] 𝕜), y (A x) = y (B x)) : A = B

@[simp]

theorem ContinuousLinearMapWOT.zero_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (x : E) : 0 x = 0

@[simp]

theorem ContinuousLinearMapWOT.add_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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) [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : (E →WOT[𝕜] F) →ₗ[𝕜] E × (F →L[𝕜] 𝕜) → 𝕜

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 × (F →L[𝕜] 𝕜)) => match x with | (x, y) => y (A x), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousLinearMapWOT.inducingFn_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {f : E →WOT[𝕜] F} {x : E} {y : F →L[𝕜] 𝕜} : (ContinuousLinearMapWOT.inducingFn 𝕜 E F) f (x, y) = y (f x)

instance ContinuousLinearMapWOT.instTopologicalSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : Continuous ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)

theorem ContinuousLinearMapWOT.continuous_dual_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (x : E) (y : F →L[𝕜] 𝕜) : 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {α : Type u_4} [TopologicalSpace α] {g : α → E →WOT[𝕜] F} (h : ∀ (x : E) (y : F →L[𝕜] 𝕜), Continuous fun (a : α) => y ((g a) x)) : Continuous g

theorem ContinuousLinearMapWOT.isInducing_inducingFn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : IsInducing ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)

theorem ContinuousLinearMapWOT.isEmbedding_inducingFn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [SeparatingDual 𝕜 F] : IsEmbedding ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)

@[deprecated ContinuousLinearMapWOT.isEmbedding_inducingFn]

theorem ContinuousLinearMapWOT.embedding_inducingFn {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [SeparatingDual 𝕜 F] : IsEmbedding ⇑(ContinuousLinearMapWOT.inducingFn 𝕜 E F)

Alias of ContinuousLinearMapWOT.isEmbedding_inducingFn.

theorem ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {α : Type u_4} {l : Filter α} {f : α → E →WOT[𝕜] F} {A : E →WOT[𝕜] F} : Filter.Tendsto f l (nhds A) ↔ ∀ (x : E) (y : F →L[𝕜] 𝕜), 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] {l : Filter (E →WOT[𝕜] F)} {A : E →WOT[𝕜] F} : l ≤ nhds A ↔ ∀ (x : E) (y : F →L[𝕜] 𝕜), 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [SeparatingDual 𝕜 F] : T3Space (E →WOT[𝕜] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMapWOT.instContinuousAdd {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : ContinuousAdd (E →WOT[𝕜] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMapWOT.instContinuousNeg {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : ContinuousNeg (E →WOT[𝕜] F)

Equations

• ⋯ = ⋯

instance ContinuousLinearMapWOT.instContinuousSMul {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : ContinuousSMul 𝕜 (E →WOT[𝕜] F)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

instance ContinuousLinearMapWOT.instUniformSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 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} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] (x : E) (y : F →L[𝕜] 𝕜) : 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) [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : SeminormFamily 𝕜 (E →WOT[𝕜] F) (E × (F →L[𝕜] 𝕜))

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_1, y) = ContinuousLinearMapWOT.seminorm x_1 y

theorem ContinuousLinearMapWOT.withSeminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : WithSeminorms (ContinuousLinearMapWOT.seminormFamily 𝕜 E F)

theorem ContinuousLinearMapWOT.hasBasis_seminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] : (nhds 0).HasBasis (ContinuousLinearMapWOT.seminormFamily 𝕜 E F).basisSets id

instance ContinuousLinearMapWOT.instLocallyConvexSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [NormedSpace ℝ 𝕜] [Module ℝ (E →WOT[𝕜] F)] [IsScalarTower ℝ 𝕜 (E →WOT[𝕜] F)] : LocallyConvexSpace ℝ (E →WOT[𝕜] F)

Equations

• ⋯ = ⋯

theorem ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [ContinuousSMul 𝕜 E] : Continuous ⇑(ContinuousLinearMap.toWOT 𝕜 E F)

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

def ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜 F] [TopologicalAddGroup F] [ContinuousConstSMul 𝕜 F] [ContinuousSMul 𝕜 E] : (E →L[𝕜] F) →L[𝕜] E →WOT[𝕜] F

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

Equations

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