Continuity and Von Neumann boundedness

This file proves that for two topological vector spaces E and F over nontrivially normed fields, if E is first countable, then every locally bounded linear map E →ₛₗ[σ] F is continuous (this is LinearMap.continuous_of_locally_bounded).

References

• [Bourbaki, Topological Vector Spaces][bourbaki1987]

def LinearMap.clmOfExistsBoundedImage {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [TopologicalSpace F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [NormedField 𝕜'] [Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] [IsTopologicalAddGroup F] (f : E →ₛₗ[σ] F) (h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)) : E →SL[σ] F

Construct a continuous linear map from a linear map f : E →ₛₗ[σ] F and the existence of a neighborhood of zero that gets mapped into a bounded set in F.

theorem LinearMap.clmOfExistsBoundedImage_coe {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [TopologicalSpace F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [NormedField 𝕜'] [Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] [IsTopologicalAddGroup F] {f : E →ₛₗ[σ] F} {h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)} : ↑(f.clmOfExistsBoundedImage h) = f

@[simp]

theorem LinearMap.clmOfExistsBoundedImage_apply {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [TopologicalSpace F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [NormedField 𝕜'] [Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] [IsTopologicalAddGroup F] {f : E →ₛₗ[σ] F} {h : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜' (⇑f '' V)} {x : E} : (f.clmOfExistsBoundedImage h) x = f x

theorem LinearMap.continuousAt_zero_of_locally_bounded {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [TopologicalSpace F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [NormedField 𝕜'] [Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] [FirstCountableTopology E] (f : E →ₛₗ[σ] F) (hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)) : ContinuousAt (⇑f) 0

theorem LinearMap.continuous_of_locally_bounded {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [TopologicalSpace E] [IsTopologicalAddGroup E] [AddCommGroup F] [TopologicalSpace F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [NormedField 𝕜'] [Module 𝕜' F] {σ : 𝕜 →+* 𝕜'} [RingHomIsometric σ] [FirstCountableTopology E] [IsTopologicalAddGroup F] (f : E →ₛₗ[σ] F) (hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s)) : Continuous ⇑f

If E is first countable, then every locally bounded linear map E →ₛₗ[σ] F is continuous.