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 #
- [Bourbaki, Topological Vector Spaces][bourbaki1987]
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 : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜 (⇑f '' V))
:
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
- LinearMap.clmOfExistsBoundedImage f 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 : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜 (⇑f '' V)}
:
↑(LinearMap.clmOfExistsBoundedImage f 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 : ∃ V ∈ nhds 0, Bornology.IsVonNBounded 𝕜 (⇑f '' V)}
{x : E}
:
(LinearMap.clmOfExistsBoundedImage f 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 𝕜 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]
[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 𝕜 s → Bornology.IsVonNBounded 𝕜' (⇑f '' s))
:
Continuous ⇑f
If E is first countable, then every locally bounded linear map E →ₛₗ[σ] F is continuous.