Montel spaces

A Montel space is a topological vector space E that has the Heine-Borel property: every closed and (von Neumann) bounded set is compact.

Note that we are not requiring that E is a barrelled space, so the usual definition of a Montel space would be [MontelSpace 𝕜 E] [BarrelledSpace 𝕜 E].

• MontelSpace.finiteDimensional_of_normedSpace: every normed Montel space is finite dimensional.
• ContinuousLinearEquiv.toCompactConvergenceCLM: if E is a Montel space then topology of compact convergence and the strong topology on E →SL[σ] F coincide. We record this as a continuous linear equivalence between E →SL[σ] F and E →SL_c[σ] F. This is Proposition 34.5 in F. Trèves.

References

• F. Trèves, Topological vector spaces, distributions and kernels

class MontelSpace (𝕜 : Type u_4) (E : Type u_5) [SeminormedRing 𝕜] [Zero E] [SMul 𝕜 E] [TopologicalSpace E] : Prop

A Montel space is a topological vector space that has the Heine-Borel property: every closed and (von Neumann) bounded set is compact.

Note that we are not requiring that E is a barrelled space, so the usual definition of a Montel space would be [MontelSpace 𝕜 E] [BarrelledSpace 𝕜 E].

• heine_borel (s : Set E) : IsClosed s → Bornology.IsVonNBounded 𝕜 s → IsCompact s

theorem MontelSpace.isCompact_of_isClosed_of_isVonNBounded (𝕜 : Type u_1) {E : Type u_2} [SeminormedRing 𝕜] [Zero E] [SMul 𝕜 E] [TopologicalSpace E] [hm : MontelSpace 𝕜 E] {s : Set E} (h_closed : IsClosed s) (h_bounded : Bornology.IsVonNBounded 𝕜 s) : IsCompact s

theorem MontelSpace.finiteDimensional_of_normedSpace {𝕜 : Type u_1} {E : Type u_2} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace 𝕜] [hM : MontelSpace 𝕜 E] : FiniteDimensional 𝕜 E

def ContinuousLinearEquiv.toCompactConvergenceCLM {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_3) (F : Type u_4) [AddCommGroup E] [Module 𝕜₁ E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] [T1Space E] [MontelSpace 𝕜₁ E] : (E →SL[σ] F) ≃L[𝕜₂] CompactConvergenceCLM σ E F

If E is a Montel space, then the strong topology on E →L[𝕜] F coincides with the topology of compact convergence.

We realize this equality in terms of a continuous linear equivalence between the type synonyms.

Equations

• ContinuousLinearEquiv.toCompactConvergenceCLM σ E F = { toLinearEquiv := LinearEquiv.toCompactConvergenceCLM✝ σ E F, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem ContinuousLinearEquiv.toCompactConvergenceCLM_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜₁ E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] [T1Space E] [MontelSpace 𝕜₁ E] (f : E →SL[σ] F) (x : E) : ((toCompactConvergenceCLM σ E F) f) x = f x

@[simp]

theorem ContinuousLinearEquiv.toCompactConvergenceCLM_symm_apply {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [Module 𝕜₁ E] [UniformSpace E] [IsUniformAddGroup E] [ContinuousSMul 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜₂ F] [T1Space E] [MontelSpace 𝕜₁ E] (f : CompactConvergenceCLM σ E F) (x : E) : ((toCompactConvergenceCLM σ E F).symm f) x = f x