Documentation

Mathlib.Analysis.LocallyConvex.ContinuousOfBounded

Continuity and Von Neumann boundedness #

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

We keep this file separate from Analysis/LocallyConvex/Bounded in order not to import Analysis/NormedSpace/RCLike there, because defining the strong topology on the space of continuous linear maps will require importing Analysis/LocallyConvex/Bounded in Analysis/NormedSpace/OperatorNorm.

References #

def LinearMap.clmOfExistsBoundedImage {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [UniformSpace E] [UniformAddGroup E] [AddCommGroup F] [UniformSpace F] [UniformAddGroup F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [ContinuousSMul 𝕜 E] (f : E →ₗ[𝕜] F) (h : Vnhds 0, Bornology.IsVonNBounded 𝕜 (f '' V)) :
E →L[𝕜] 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.

Equations
  • f.clmOfExistsBoundedImage h = { toLinearMap := f, cont := }
Instances For
    theorem LinearMap.clmOfExistsBoundedImage_coe {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [UniformSpace E] [UniformAddGroup E] [AddCommGroup F] [UniformSpace F] [UniformAddGroup F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [ContinuousSMul 𝕜 E] {f : E →ₗ[𝕜] F} {h : Vnhds 0, Bornology.IsVonNBounded 𝕜 (f '' V)} :
    (f.clmOfExistsBoundedImage h) = f
    @[simp]
    theorem LinearMap.clmOfExistsBoundedImage_apply {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [AddCommGroup E] [UniformSpace E] [UniformAddGroup E] [AddCommGroup F] [UniformSpace F] [UniformAddGroup F] [NontriviallyNormedField 𝕜] [Module 𝕜 E] [Module 𝕜 F] [ContinuousSMul 𝕜 E] {f : E →ₗ[𝕜] F} {h : Vnhds 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] [UniformSpace E] [UniformAddGroup E] [AddCommGroup F] [UniformSpace F] [FirstCountableTopology E] [RCLike 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [RCLike 𝕜'] [Module 𝕜' F] [ContinuousSMul 𝕜' F] {σ : 𝕜 →+* 𝕜'} (f : E →ₛₗ[σ] F) (hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 sBornology.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] [UniformSpace E] [UniformAddGroup E] [AddCommGroup F] [UniformSpace F] [FirstCountableTopology E] [RCLike 𝕜] [Module 𝕜 E] [ContinuousSMul 𝕜 E] [RCLike 𝕜'] [Module 𝕜' F] [ContinuousSMul 𝕜' F] {σ : 𝕜 →+* 𝕜'} [UniformAddGroup F] (f : E →ₛₗ[σ] F) (hf : ∀ (s : Set E), Bornology.IsVonNBounded 𝕜 sBornology.IsVonNBounded 𝕜' (f '' s)) :

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