Topology of compact convergence on the space of continuous linear maps

In this file, we define a type alias CompactConvergenceCLM for E →L[𝕜] F, endowed with the topology of uniform convergence on compact subsets.

More concretely, CompactConvergenceCLM is an abbreviation for UniformConvergenceCLM σ F {(S : Set E) | IsCompact S}. We denote it by E →SL_c[σ] F.

Here is a list of type aliases for E →L[𝕜] F endowed with various topologies :

• ContinuousLinearMap: topology of bounded convergence
• UniformConvergenceCLM: topology of 𝔖-convergence, for a general 𝔖 : Set (Set E)
• CompactConvergenceCLM: topology of compact convergence
• PointwiseConvergenceCLM: topology of pointwise convergence, also called "weak-* topology" or "strong-operator topology" depending on the context
• ContinuousLinearMapWOT: topology of weak pointwise convergence, also called "weak-operator topology"

References

• [N. Bourbaki, Topological Vector Spaces][bourbaki1987]

Tags

uniform convergence, bounded convergence

Topology of compact convergence for continuous linear maps

@[reducible, inline]

abbrev CompactConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_4) (F : Type u_5) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] : Type (max u_4 u_5)

The topology of compact convergence on E →L[𝕜] F.

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

The topology of compact convergence on E →L[𝕜] F.

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

The topology of compact convergence on E →L[𝕜] F.

instance CompactConvergenceCLM.continuousSMul {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [RingHomSurjective σ] [RingHomIsometric σ] [UniformSpace E] [IsUniformAddGroup E] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₁ E] [ContinuousSMul 𝕜₂ F] : ContinuousSMul 𝕜₂ (CompactConvergenceCLM σ E F)

instance CompactConvergenceCLM.instContinuousEvalConst {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] : ContinuousEvalConst (CompactConvergenceCLM σ E F) E F

instance CompactConvergenceCLM.instT2Space {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] [T2Space F] : T2Space (CompactConvergenceCLM σ E F)

theorem CompactConvergenceCLM.hasBasis_nhds_zero_of_basis {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] {ι : Type u_7} {p : ι → Prop} {b : ι → Set F} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun (Si : Set E × ι) => IsCompact Si.1 ∧ p Si.2) fun (Si : Set E × ι) => {f : CompactConvergenceCLM σ E F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem CompactConvergenceCLM.hasBasis_nhds_zero {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_4} {F : Type u_5} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] [IsTopologicalAddGroup F] : (nhds 0).HasBasis (fun (SV : Set E × Set F) => IsCompact SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : CompactConvergenceCLM σ E F | ∀ x ∈ SV.1, f x ∈ SV.2}

def ContinuousLinearMap.precompCompactConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} (G : Type u_6) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) : CompactConvergenceCLM τ F G →L[𝕜₃] CompactConvergenceCLM ρ E G

Specialization of ContinuousLinearMap.precomp_uniformConvergenceCLM to compact convergence.

@[simp]

theorem ContinuousLinearMap.precompCompactConvergenceCLM_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} (G : Type u_6) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (f : UniformConvergenceCLM τ G {S : Set F | IsCompact S}) : (precompCompactConvergenceCLM G L) f = comp f L

@[deprecated ContinuousLinearMap.precompCompactConvergenceCLM (since := "2026-01-27")]

def precomp_compactConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} (G : Type u_6) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) : CompactConvergenceCLM τ F G →L[𝕜₃] CompactConvergenceCLM ρ E G

Alias of ContinuousLinearMap.precompCompactConvergenceCLM.

---

Specialization of ContinuousLinearMap.precomp_uniformConvergenceCLM to compact convergence.

@[deprecated ContinuousLinearMap.precompCompactConvergenceCLM_apply (since := "2026-01-27")]

theorem precomp_compactConvergenceCLM_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] {E : Type u_4} {F : Type u_5} (G : Type u_6) [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] (L : E →SL[σ] F) (f : UniformConvergenceCLM τ G {S : Set F | IsCompact S}) : (ContinuousLinearMap.precompCompactConvergenceCLM G L) f = ContinuousLinearMap.comp f L

Alias of ContinuousLinearMap.precompCompactConvergenceCLM_apply.

def ContinuousLinearMap.postcompCompactConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : CompactConvergenceCLM σ E F →SL[τ] CompactConvergenceCLM ρ E G

Specialization of ContinuousLinearMap.postcomp_uniformConvergenceCLM to compact convergence.

@[simp]

theorem ContinuousLinearMap.postcompCompactConvergenceCLM_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F {S : Set E | IsCompact S}) : (postcompCompactConvergenceCLM E L) f = L.comp f

@[deprecated ContinuousLinearMap.postcompCompactConvergenceCLM (since := "2026-01-27")]

def postcomp_compactConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) : CompactConvergenceCLM σ E F →SL[τ] CompactConvergenceCLM ρ E G

Alias of ContinuousLinearMap.postcompCompactConvergenceCLM.

---

Specialization of ContinuousLinearMap.postcomp_uniformConvergenceCLM to compact convergence.

@[deprecated ContinuousLinearMap.postcompCompactConvergenceCLM_apply (since := "2026-01-27")]

theorem postcomp_compactConvergenceCLM_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₂ →+* 𝕜₃} {ρ : 𝕜₁ →+* 𝕜₃} [RingHomCompTriple σ τ ρ] (E : Type u_4) {F : Type u_5} {G : Type u_6} [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [AddCommGroup G] [Module 𝕜₃ G] [TopologicalSpace E] [TopologicalSpace F] [TopologicalSpace G] [IsTopologicalAddGroup F] [IsTopologicalAddGroup G] [ContinuousConstSMul 𝕜₃ G] [ContinuousConstSMul 𝕜₂ F] (L : F →SL[τ] G) (f : UniformConvergenceCLM σ F {S : Set E | IsCompact S}) : (ContinuousLinearMap.postcompCompactConvergenceCLM E L) f = L.comp f

Alias of ContinuousLinearMap.postcompCompactConvergenceCLM_apply.