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.

structure 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 →SL[σ] F endowed with the weak operator topology, denoted as E →SWOT[σ] F. Likewise, when σ := RingHom.id 𝕜, the notation E →WOT[𝕜] F is available.

• ofCLM :: (
• toCLM : E →SL[σ] F

  The continuous linear map underlying an element of E →SWOT[σ] F.

• )

def ContinuousLinearMapWOT.delabOfCLM : Lean.PrettyPrinter.Delaborator.Delab

This prevents ofCLM A being printed as { toCLM := x } by delabStructureInstance.

Equations

• ContinuousLinearMapWOT.delabOfCLM = Lean.PrettyPrinter.Delaborator.delabApp

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

The type copy of E →SL[σ] F endowed with the weak operator topology, denoted as E →SWOT[σ] F. Likewise, when σ := RingHom.id 𝕜, the notation E →WOT[𝕜] F is available.

Equations

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

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

The type copy of E →SL[σ] F endowed with the weak operator topology, denoted as E →SWOT[σ] F. Likewise, when σ := RingHom.id 𝕜, the notation E →WOT[𝕜] F is available.

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.

def ContinuousLinearMapWOT.equiv {𝕜₁ : 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] : (E →SWOT[σ] F) ≃ (E →SL[σ] F)

The equivalence between ContinuousLinearMapWOT and ContinuousLinearMap.

Equations

• ContinuousLinearMapWOT.equiv = { toFun := ContinuousLinearMapWOT.toCLM, invFun := ContinuousLinearMapWOT.ofCLM, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem ContinuousLinearMapWOT.equiv_symm_apply_toCLM {𝕜₁ : 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] (toCLM : E →SL[σ] F) : (equiv.symm toCLM).toCLM = toCLM

@[simp]

theorem ContinuousLinearMapWOT.equiv_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] (self : E →SWOT[σ] F) : equiv self = self.toCLM

@[simp]

theorem ContinuousLinearMapWOT.toCLM_injective {𝕜₁ : 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] : Function.Injective toCLM

@[simp]

theorem ContinuousLinearMapWOT.toCLM_surjective {𝕜₁ : 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] : Function.Surjective toCLM

theorem ContinuousLinearMapWOT.toCLM_bijective {𝕜₁ : 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] : Function.Bijective toCLM

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_injective {𝕜₁ : 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] : Function.Injective ofCLM

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_surjective {𝕜₁ : 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] : Function.Surjective ofCLM

theorem ContinuousLinearMapWOT.ofCLM_bijective {𝕜₁ : 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] : Function.Bijective ofCLM

@[implicit_reducible]

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 = ContinuousLinearMapWOT.equiv.addCommGroup

@[implicit_reducible]

instance ContinuousLinearMapWOT.instSMul {𝕜₁ : 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] {S : Type u_5} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] : SMul S (E →SWOT[σ] F)

Equations

• ContinuousLinearMapWOT.instSMul = Equiv.smul S ContinuousLinearMapWOT.equiv

@[implicit_reducible]

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] {S : Type u_5} [Semiring S] [Module S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [IsTopologicalAddGroup F] : Module S (E →SWOT[σ] F)

Equations

• ContinuousLinearMapWOT.instModule = Equiv.module S ContinuousLinearMapWOT.equiv

instance ContinuousLinearMapWOT.instIsScalarTower {𝕜₁ : 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] {S : Type u_5} {T : Type u_6} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [DistribSMul T F] [SMulCommClass 𝕜₂ T F] [ContinuousConstSMul T F] [SMul S T] [IsScalarTower S T F] : IsScalarTower S T (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instSMulCommClass {𝕜₁ : 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] {S : Type u_5} {T : Type u_6} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [DistribSMul T F] [SMulCommClass 𝕜₂ T F] [ContinuousConstSMul T F] [SMulCommClass S T F] : SMulCommClass S T (E →SWOT[σ] F)

instance ContinuousLinearMapWOT.instIsCentralScalar {𝕜₁ : 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] {S : Type u_5} [Semiring S] [Module S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [Module Sᵐᵒᵖ F] [IsCentralScalar S F] : IsCentralScalar S (E →SWOT[σ] F)

@[implicit_reducible]

instance ContinuousLinearMapWOT.instRing {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [IsTopologicalAddGroup E] : Ring (E →WOT[𝕜₁] E)

Equations

• ContinuousLinearMapWOT.instRing = ContinuousLinearMapWOT.equiv.ring

@[implicit_reducible]

instance ContinuousLinearMapWOT.instAlgebra {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] {S : Type u_5} [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] : Algebra S (E →WOT[𝕜₁] E)

Equations

• ContinuousLinearMapWOT.instAlgebra = Equiv.algebra S ContinuousLinearMapWOT.equiv

def ContinuousLinearMapWOT.addEquiv {𝕜₁ : 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] : (E →SWOT[σ] F) ≃+ (E →SL[σ] F)

The additive group equivalence between ContinuousLinearMapWOT and ContinuousLinearMap.

Equations

• ContinuousLinearMapWOT.addEquiv = ContinuousLinearMapWOT.equiv.addEquiv

@[simp]

theorem ContinuousLinearMapWOT.addEquiv_symm_apply_toCLM {𝕜₁ : 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] (toCLM : E →SL[σ] F) : (addEquiv.symm toCLM).toCLM = toCLM

@[simp]

theorem ContinuousLinearMapWOT.addEquiv_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] (self : E →SWOT[σ] F) : addEquiv self = self.toCLM

def ContinuousLinearMapWOT.linearEquiv {𝕜₁ : 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] (S : Type u_5) [Semiring S] [Module S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [IsTopologicalAddGroup F] : (E →SWOT[σ] F) ≃ₗ[S] E →SL[σ] F

The linear equivalence between ContinuousLinearMapWOT and ContinuousLinearMap.

Equations

• ContinuousLinearMapWOT.linearEquiv S = Equiv.linearEquiv S ContinuousLinearMapWOT.equiv

@[simp]

theorem ContinuousLinearMapWOT.linearEquiv_symm_apply_toCLM {𝕜₁ : 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] (S : Type u_5) [Semiring S] [Module S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [IsTopologicalAddGroup F] (a✝ : E →SL[σ] F) : ((linearEquiv S).symm a✝).toCLM = a✝

@[simp]

theorem ContinuousLinearMapWOT.linearEquiv_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] (S : Type u_5) [Semiring S] [Module S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [IsTopologicalAddGroup F] (a✝ : E →SWOT[σ] F) : (linearEquiv S) a✝ = a✝.toCLM

def ContinuousLinearMapWOT.ringEquiv {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [IsTopologicalAddGroup E] : (E →WOT[𝕜₁] E) ≃+* (E →L[𝕜₁] E)

The ring equivalence between ContinuousLinearMapWOT and ContinuousLinearMap.

Equations

• ContinuousLinearMapWOT.ringEquiv = ContinuousLinearMapWOT.equiv.ringEquiv

@[simp]

theorem ContinuousLinearMapWOT.ringEquiv_symm_apply_toCLM {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [IsTopologicalAddGroup E] (toCLM : E →L[𝕜₁] E) : (ringEquiv.symm toCLM).toCLM = toCLM

@[simp]

theorem ContinuousLinearMapWOT.ringEquiv_apply {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [IsTopologicalAddGroup E] (self : E →WOT[𝕜₁] E) : ringEquiv self = self.toCLM

def ContinuousLinearMapWOT.algEquiv {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] (S : Type u_5) [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] : (E →WOT[𝕜₁] E) ≃ₐ[S] E →L[𝕜₁] E

The algebra equivalence between ContinuousLinearMapWOT and ContinuousLinearMap.

Equations

• ContinuousLinearMapWOT.algEquiv S = Equiv.algEquiv S ContinuousLinearMapWOT.equiv

@[simp]

theorem ContinuousLinearMapWOT.algEquiv_symm_apply_toCLM {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] (S : Type u_5) [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] (toCLM : E →L[𝕜₁] E) : ((algEquiv S).symm toCLM).toCLM = toCLM

@[simp]

theorem ContinuousLinearMapWOT.algEquiv_apply {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] (S : Type u_5) [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] (self : E →WOT[𝕜₁] E) : (algEquiv S) self = self.toCLM

@[implicit_reducible]

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] : FunLike (E →SWOT[σ] F) E F

Equations

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

@[simp]

theorem ContinuousLinearMapWOT.coe_toCLM {𝕜₁ : 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] (A : E →SWOT[σ] F) : ⇑A.toCLM = ⇑A

@[simp]

theorem ContinuousLinearMapWOT.coe_ofCLM {𝕜₁ : 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] (A : E →SL[σ] F) : ⇑(ofCLM A) = ⇑A

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] : ContinuousSemilinearMapClass (E →SWOT[σ] F) σ E F

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_toCLM {𝕜₁ : 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] (A : E →SWOT[σ] F) : ofCLM A.toCLM = A

theorem ContinuousLinearMapWOT.toCLM_ofCLM {𝕜₁ : 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] (A : E →SL[σ] F) : (ofCLM A).toCLM = A

@[simp]

theorem ContinuousLinearMapWOT.toCLM_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] {A : E →SWOT[σ] F} {x : E} : A.toCLM x = A x

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_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] {A : E →SL[σ] F} {x : E} : (ofCLM A) x = A x

@[deprecated ContinuousLinearMapWOT.ofCLM_apply (since := "2026-04-10")]

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] {A : E →SL[σ] F} {x : E} : (ContinuousLinearMapWOT.ofCLM A) x = A x

Alias of ContinuousLinearMapWOT.ofCLM_apply.

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] {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] {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] [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] [H : SeparatingDual 𝕜₂ F] {A B : E →SWOT[σ] F} : A = B ↔ ∀ (x : E) (y : StrongDual 𝕜₂ F), y (A x) = y (B x)

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_smul {𝕜₁ : 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] {S : Type u_5} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] {c : S} {f : E →SL[σ] F} : ofCLM (c • f) = c • ofCLM f

@[simp]

theorem ContinuousLinearMapWOT.toCLM_smul {𝕜₁ : 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] {S : Type u_5} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] {c : S} {f : E →SWOT[σ] F} : (c • f).toCLM = c • f.toCLM

@[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] {S : Type u_5} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] {f : E →SWOT[σ] F} (c : S) (x : E) : (c • f) x = c • f x

@[simp]

theorem ContinuousLinearMapWOT.toCLM_algebraMap {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] {S : Type u_5} [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] (c : S) : ((algebraMap S (E →WOT[𝕜₁] E)) c).toCLM = (algebraMap S (E →L[𝕜₁] E)) c

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_algebraMap {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] {S : Type u_5} [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] (c : S) : ofCLM ((algebraMap S (E →L[𝕜₁] E)) c) = (algebraMap S (E →WOT[𝕜₁] E)) c

@[simp]

theorem ContinuousLinearMapWOT.algebraMapCLM_apply {𝕜₁ : Type u_1} [NormedField 𝕜₁] {E : Type u_3} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] {S : Type u_5} [CommSemiring S] [Module S E] [SMulCommClass 𝕜₁ S E] [SMul S 𝕜₁] [IsScalarTower S 𝕜₁ E] [ContinuousConstSMul S E] [IsTopologicalAddGroup E] (c : S) (x : E) : ((algebraMap S (E →WOT[𝕜₁] E)) c) x = c • x

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_zero {𝕜₁ : 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] : ofCLM 0 = 0

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_add {𝕜₁ : 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] {f g : E →SL[σ] F} : ofCLM (f + g) = ofCLM f + ofCLM g

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_sub {𝕜₁ : 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] {f g : E →SL[σ] F} : ofCLM (f - g) = ofCLM f - ofCLM g

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_neg {𝕜₁ : 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] {f : E →SL[σ] F} : ofCLM (-f) = -ofCLM f

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_mul {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (f g : F →L[𝕜₂] F) : ofCLM (f * g) = ofCLM f * ofCLM g

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_one {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] : ofCLM 1 = 1

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_pow {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (f : F →L[𝕜₂] F) (n : ℕ) : ofCLM (f ^ n) = ofCLM f ^ n

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_natCast {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (n : ℕ) : ofCLM ↑n = ↑n

@[simp]

theorem ContinuousLinearMapWOT.ofCLM_intCast {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (n : ℤ) : ofCLM ↑n = ↑n

@[simp]

theorem ContinuousLinearMapWOT.toCLM_zero {𝕜₁ : 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] : toCLM 0 = 0

@[simp]

theorem ContinuousLinearMapWOT.toCLM_add {𝕜₁ : 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] {f g : E →SWOT[σ] F} : (f + g).toCLM = f.toCLM + g.toCLM

@[simp]

theorem ContinuousLinearMapWOT.toCLM_sub {𝕜₁ : 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] {f g : E →SWOT[σ] F} : (f - g).toCLM = f.toCLM - g.toCLM

@[simp]

theorem ContinuousLinearMapWOT.toCLM_neg {𝕜₁ : 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] {f : E →SWOT[σ] F} : (-f).toCLM = -f.toCLM

@[simp]

theorem ContinuousLinearMapWOT.toCLM_mul {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (f g : F →WOT[𝕜₂] F) : (f * g).toCLM = f.toCLM * g.toCLM

@[simp]

theorem ContinuousLinearMapWOT.toCLM_one {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] : toCLM 1 = 1

@[simp]

theorem ContinuousLinearMapWOT.toCLM_pow {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (f : F →WOT[𝕜₂] F) (n : ℕ) : (f ^ n).toCLM = f.toCLM ^ n

@[simp]

theorem ContinuousLinearMapWOT.toCLM_natCast {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (n : ℕ) : (↑n).toCLM = ↑n

@[simp]

theorem ContinuousLinearMapWOT.toCLM_intCast {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (n : ℤ) : (↑n).toCLM = ↑n

@[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] (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] {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] {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] {f : E →SWOT[σ] F} (x : E) : (-f) x = -f x

@[simp]

theorem ContinuousLinearMapWOT.mul_apply {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (f g : F →WOT[𝕜₂] F) (x : F) : (f * g) x = f (g x)

@[simp]

theorem ContinuousLinearMapWOT.one_apply {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (x : F) : 1 x = x

@[simp]

theorem ContinuousLinearMapWOT.natCast_apply {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (n : ℕ) (x : F) : ↑n x = n • x

@[simp]

theorem ContinuousLinearMapWOT.intCast_apply {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (n : ℤ) (x : F) : ↑n x = n • 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)

@[implicit_reducible]

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.instContinuousConstSMulIdOfIsScalarTower {𝕜₂ : Type u_2} [NormedField 𝕜₂] {F : Type u_4} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] {S : Type u_5} [DistribSMul S F] [SMulCommClass 𝕜₂ S F] [ContinuousConstSMul S F] [SMul S 𝕜₂] [IsScalarTower S 𝕜₂ 𝕜₂] [IsScalarTower S 𝕜₂ F] : ContinuousConstSMul S (F →WOT[𝕜₂] 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] {S : Type u_5} [Semiring S] [Module S F] [SMulCommClass 𝕜₂ S F] [Module S 𝕜₂] [IsScalarTower S 𝕜₂ F] [IsScalarTower S 𝕜₂ 𝕜₂] [ContinuousConstSMul S F] [TopologicalSpace S] [ContinuousSMul S 𝕜₂] : ContinuousSMul S (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)

@[implicit_reducible]

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 (fun (x : Set (E →SWOT[σ] F)) => x ∈ (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.continuous_ofCLM {𝕜₁ : 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 ofCLM

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

@[deprecated ContinuousLinearMapWOT.continuous_ofCLM (since := "2026-04-10")]

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 ofCLM

Alias of ContinuousLinearMapWOT.continuous_ofCLM.

---

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

def ContinuousLinearMap.WOTofCLM {𝕜₁ : 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

• ContinuousLinearMap.WOTofCLM = { toLinearMap := ↑(ContinuousLinearMapWOT.linearEquiv 𝕜₂).symm, cont := ⋯ }

@[deprecated ContinuousLinearMap.WOTofCLM (since := "2026-04-10")]

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

Alias of ContinuousLinearMap.WOTofCLM.

---

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

Equations

• @ContinuousLinearMapWOT.ContinuousLinearMap.toWOTCLM = @ContinuousLinearMap.WOTofCLM

def ContinuousLinearMapWOT.id (𝕜₂ : Type u_6) (F : Type u_10) [NormedField 𝕜₂] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] : F →WOT[𝕜₂] F

The identity as a continuous linear map on the type synonym equipped with the weak operator topology

Equations

• ContinuousLinearMapWOT.id 𝕜₂ F = ContinuousLinearMapWOT.ofCLM (ContinuousLinearMap.id 𝕜₂ F)

@[simp]

theorem ContinuousLinearMapWOT.toCLM_id {𝕜₂ : Type u_6} {F : Type u_10} [NormedField 𝕜₂] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] : (ContinuousLinearMapWOT.id 𝕜₂ F).toCLM = ContinuousLinearMap.id 𝕜₂ F

def ContinuousLinearMapWOT.comp {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G) (f : E →SWOT[σ₁₂] F) : E →SWOT[σ₁₃] G

Composition of continuous linear maps on the type synonym equipped with the weak operator topology.

Equations

• g.comp f = ContinuousLinearMapWOT.ofCLM (g.toCLM.comp f.toCLM)

@[simp]

theorem ContinuousLinearMapWOT.comp_apply {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G) (f : E →SWOT[σ₁₂] F) (x : E) : (g.comp f) x = g (f x)

@[simp]

theorem ContinuousLinearMapWOT.toCLM_comp {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G) (f : E →SWOT[σ₁₂] F) : (g.comp f).toCLM = g.toCLM.comp f.toCLM

@[simp]

theorem ContinuousLinearMapWOT.comp_id {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {E : Type u_9} {F : Type u_10} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] (f : E →SWOT[σ₁₂] F) : (ContinuousLinearMapWOT.id 𝕜₂ F).comp f = f

@[simp]

theorem ContinuousLinearMapWOT.id_comp {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₂₃ : 𝕜₂ →+* 𝕜₃} [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] (g : F →SWOT[σ₂₃] G) : g.comp (ContinuousLinearMapWOT.id 𝕜₂ F) = g

theorem ContinuousLinearMapWOT.comp_assoc {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {𝕜₄ : Type u_8} {E : Type u_9} {F : Type u_10} {G : Type u_11} {H : Type u_12} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] [NormedField 𝕜₄] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₁₄ : 𝕜₁ →+* 𝕜₄} {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₂₄ : 𝕜₂ →+* 𝕜₄} {σ₃₄ : 𝕜₃ →+* 𝕜₄} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [RingHomCompTriple σ₁₃ σ₃₄ σ₁₄] [RingHomCompTriple σ₁₂ σ₂₄ σ₁₄] [RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [AddCommGroup H] [TopologicalSpace H] [Module 𝕜₄ H] (g₃₄ : G →SWOT[σ₃₄] H) (g₂₃ : F →SWOT[σ₂₃] G) (g₁₂ : E →SWOT[σ₁₂] F) : (g₃₄.comp g₂₃).comp g₁₂ = g₃₄.comp (g₂₃.comp g₁₂)

theorem ContinuousLinearMapWOT.mul_eq_comp {𝕜₂ : Type u_6} {F : Type u_10} [NormedField 𝕜₂] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] (f g : F →WOT[𝕜₂] F) : f * g = f.comp g

theorem ContinuousLinearMapWOT.continuous_precomp {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (f : E →SWOT[σ₁₂] F) : Continuous fun (g : F →SWOT[σ₂₃] G) => g.comp f

theorem ContinuousLinearMapWOT.continuous_postcomp {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ₂₃] [RingHomIsometric σ₂₃] (g : F →SWOT[σ₂₃] G) : Continuous fun (f : E →SWOT[σ₁₂] F) => g.comp f

While RingHomSurjective σ₂₃ is not a strict requirement, there are obstructions to this without any assumption on σ₂₃ (in particular, on the dimension of the extension of 𝕜₃ over σ₂₃(𝕜₂)), and in the only common case, which is when σ₂₃ is conjugation, this type class is guaranteed. Likewise, it would suffice if RingHomIsometric were replaced with the weaker Continuous σ₂₃, but we opt for this because we have these type classes available.

def ContinuousLinearMapWOT.precompCLM {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (f : E →SWOT[σ₁₂] F) : (F →SWOT[σ₂₃] G) →L[𝕜₃] E →SWOT[σ₁₃] G

Precomposition by a fixed continuous linear map, as a continuous linear map when all spaces of continuous linear maps are equipped with the weak operator topology.

Equations

• f.precompCLM = { toFun := fun (g : F →SWOT[σ₂₃] G) => g.comp f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMapWOT.precompCLM_apply {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (f : E →SWOT[σ₁₂] F) (g : F →SWOT[σ₂₃] G) : f.precompCLM g = g.comp f

def ContinuousLinearMapWOT.postcompCLM {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ₂₃] [RingHomIsometric σ₂₃] (g : F →SWOT[σ₂₃] G) : (E →SWOT[σ₁₂] F) →SL[σ₂₃] E →SWOT[σ₁₃] G

Precomposition by a fixed continuous linear map, as a continuous linear map when all spaces of continuous linear maps are equipped with the weak operator topology.

Equations

• g.postcompCLM = { toFun := fun (f : E →SWOT[σ₁₂] F) => g.comp f, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }

@[simp]

theorem ContinuousLinearMapWOT.postcompCLM_apply {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [AddCommGroup G] [TopologicalSpace G] [Module 𝕜₃ G] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [RingHomSurjective σ₂₃] [RingHomIsometric σ₂₃] (g : F →SWOT[σ₂₃] G) (f : E →SWOT[σ₁₂] F) : g.postcompCLM f = g.comp f

instance ContinuousLinearMapWOT.instIsSemitopologicalRingId {𝕜₂ : Type u_6} {F : Type u_10} [NormedField 𝕜₂] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₂ F] [IsTopologicalAddGroup F] [ContinuousConstSMul 𝕜₂ F] : IsSemitopologicalRing (F →WOT[𝕜₂] F)