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 : StrongDual 𝕜 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 : StrongDual 𝕜 F.

Main declarations

• ContinuousLinearMapWOT σ E F: The type copy of E →SL[σ] 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 →SL[σ] 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 : StrongDual 𝕜 F.

Notation

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

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} {𝕜₂ : Type u_2} [Semiring 𝕜₁] [Semiring 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_3) (F : Type u_4) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] : Type (max u_3 u_4)

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

Equations

• (E →SWOT[σ] F) = (E →SL[σ] F)

def «term_→SWOT[_]_» : 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.

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} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] : AddCommGroup (E →SWOT[σ] F)

Equations

• ContinuousLinearMapWOT.instAddCommGroup = inferInstanceAs (AddCommGroup (E →SL[σ] F))

instance ContinuousLinearMapWOT.instModule {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : Module 𝕜₂ (E →SWOT[σ] F)

Equations

• ContinuousLinearMapWOT.instModule = inferInstanceAs (Module 𝕜₂ (E →SL[σ] F))

def ContinuousLinearMap.toWOT {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_3) (F : Type u_4) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : (E →SL[σ] F) ≃ₗ[𝕜₂] E →SWOT[σ] 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 →SL[σ] F)

instance ContinuousLinearMapWOT.instFunLike {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : FunLike (E →SWOT[σ] F) E F

Equations

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

instance ContinuousLinearMapWOT.instContinuousLinearMapClass {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : ContinuousSemilinearMapClass (E →SWOT[σ] F) σ E F

@[simp]

theorem ContinuousLinearMap.toWOT_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {A : E →SL[σ] F} {x : E} : ((toWOT σ E F) A) x = A x

theorem ContinuousLinearMapWOT.ext {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {A B : E →SWOT[σ] F} (h : ∀ (x : E), A x = B x) : A = B

theorem ContinuousLinearMapWOT.ext_iff {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {A B : E →SWOT[σ] F} : A = B ↔ ∀ (x : E), A x = B x

theorem ContinuousLinearMapWOT.ext_dual {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [H : SeparatingDual 𝕜₂ F] {A B : E →SWOT[σ] F} (h : ∀ (x : E) (y : StrongDual 𝕜₂ F), y (A x) = y (B x)) : A = B

theorem ContinuousLinearMapWOT.ext_dual_iff {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [H : SeparatingDual 𝕜₂ F] {A B : E →SWOT[σ] F} : A = B ↔ ∀ (x : E) (y : StrongDual 𝕜₂ F), y (A x) = y (B x)

@[simp]

theorem ContinuousLinearMapWOT.zero_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] (x : E) : 0 x = 0

@[simp]

theorem ContinuousLinearMapWOT.add_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {f g : E →SWOT[σ] F} (x : E) : (f + g) x = f x + g x

@[simp]

theorem ContinuousLinearMapWOT.sub_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {f g : E →SWOT[σ] F} (x : E) : (f - g) x = f x - g x

@[simp]

theorem ContinuousLinearMapWOT.neg_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {f : E →SWOT[σ] F} (x : E) : (-f) x = -f x

@[simp]

theorem ContinuousLinearMapWOT.smul_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {f : E →SWOT[σ] 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} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_3) (F : Type u_4) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : (E →SWOT[σ] F) →ₗ[𝕜₂] E × StrongDual 𝕜₂ 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 →SWOT[σ] F) (x : E × StrongDual 𝕜₂ F) => match x with | (x, y) => y (A x), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ContinuousLinearMapWOT.inducingFn_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {f : E →SWOT[σ] F} {x : E} {y : StrongDual 𝕜₂ F} : (inducingFn σ E F) f (x, y) = y (f x)

instance ContinuousLinearMapWOT.instTopologicalSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : TopologicalSpace (E →SWOT[σ] 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} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : Continuous ⇑(inducingFn σ E F)

theorem ContinuousLinearMapWOT.continuous_dual_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] (x : E) (y : StrongDual 𝕜₂ F) : Continuous fun (A : E →SWOT[σ] F) => y (A x)

theorem ContinuousLinearMapWOT.continuous_of_dual_apply_continuous {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {α : Type u_5} [TopologicalSpace α] {g : α → E →SWOT[σ] F} (h : ∀ (x : E) (y : StrongDual 𝕜₂ F), Continuous fun (a : α) => y ((g a) x)) : Continuous g

theorem ContinuousLinearMapWOT.isInducing_inducingFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : Topology.IsInducing ⇑(inducingFn σ E F)

theorem ContinuousLinearMapWOT.isEmbedding_inducingFn {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [SeparatingDual 𝕜₂ F] : Topology.IsEmbedding ⇑(inducingFn σ E F)

theorem ContinuousLinearMapWOT.tendsto_iff_forall_dual_apply_tendsto {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {α : Type u_5} {l : Filter α} {f : α → E →SWOT[σ] F} {A : E →SWOT[σ] F} : Filter.Tendsto f l (nhds A) ↔ ∀ (x : E) (y : StrongDual 𝕜₂ 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} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {l : Filter (E →SWOT[σ] F)} {A : E →SWOT[σ] F} : l ≤ nhds A ↔ ∀ (x : E) (y : StrongDual 𝕜₂ F), Filter.map (fun (T : E →SWOT[σ] F) => y (T x)) l ≤ nhds (y (A x))

instance ContinuousLinearMapWOT.instT3Space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [SeparatingDual 𝕜₂ F] : T3Space (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instContinuousAdd {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : ContinuousAdd (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instContinuousNeg {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : ContinuousNeg (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instContinuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instIsTopologicalAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : IsTopologicalAddGroup (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instUniformSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : UniformSpace (E →SWOT[σ] F)

Equations

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

instance ContinuousLinearMapWOT.instIsUniformAddGroup {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : IsUniformAddGroup (E →SWOT[σ] F)

The WOT is induced by a family of seminorms

def ContinuousLinearMapWOT.seminorm {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] (x : E) (y : StrongDual 𝕜₂ F) : Seminorm 𝕜₂ (E →SWOT[σ] 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 →SWOT[σ] F) => ‖y (A x)‖, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯, smul' := ⋯ }

def ContinuousLinearMapWOT.seminormFamily {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_3) (F : Type u_4) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : SeminormFamily 𝕜₂ (E →SWOT[σ] F) (E × StrongDual 𝕜₂ 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_1, y) = ContinuousLinearMapWOT.seminorm x_1 y

theorem ContinuousLinearMapWOT.withSeminorms {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : WithSeminorms (seminormFamily σ E F)

theorem ContinuousLinearMapWOT.hasBasis_seminorms {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : (nhds 0).HasBasis (seminormFamily σ E F).basisSets id

instance ContinuousLinearMapWOT.instLocallyConvexSpace {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [NormedSpace ℝ 𝕜₂] [Module ℝ (E →SWOT[σ] F)] [IsScalarTower ℝ 𝕜₂ (E →SWOT[σ] F)] : LocallyConvexSpace ℝ (E →SWOT[σ] F)

theorem ContinuousLinearMapWOT.ContinuousLinearMap.continuous_toWOT {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup 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} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [ContinuousSMul 𝕜₁ E] : (E →SL[σ] F) →L[𝕜₂] E →SWOT[σ] 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 := ⋯ }