Continuity and Von Neumann boundedness #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 linear_map.continuous_of_locally_bounded).

We keep this file separate from analysis/locally_convex/bounded in order not to import analysis/normed_space/is_R_or_C there, because defining the strong topology on the space of continuous linear maps will require importing analysis/locally_convex/bounded in analysis/normed_space/operator_norm.

References #

Bourbaki, Topological Vector Spaces

source

def linear_map.clm_of_exists_bounded_image {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [add_comm_group E] [uniform_space E] [uniform_add_group E] [add_comm_group F] [uniform_space F] [uniform_add_group F] [nontrivially_normed_field 𝕜] [module 𝕜 E] [module 𝕜 F] [has_continuous_smul 𝕜 E] (f : E →ₗ[𝕜] F) (h : ∃ (V : set E) (hV : V ∈ nhds 0), bornology.is_vonN_bounded 𝕜 (⇑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.clm_of_exists_bounded_image h = {to_linear_map := f, cont := _}

source

theorem linear_map.clm_of_exists_bounded_image_coe {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [add_comm_group E] [uniform_space E] [uniform_add_group E] [add_comm_group F] [uniform_space F] [uniform_add_group F] [nontrivially_normed_field 𝕜] [module 𝕜 E] [module 𝕜 F] [has_continuous_smul 𝕜 E] {f : E →ₗ[𝕜] F} {h : ∃ (V : set E) (hV : V ∈ nhds 0), bornology.is_vonN_bounded 𝕜 (⇑f '' V)} :

↑(f.clm_of_exists_bounded_image h) = f

source

@[simp]

theorem linear_map.clm_of_exists_bounded_image_apply {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} [add_comm_group E] [uniform_space E] [uniform_add_group E] [add_comm_group F] [uniform_space F] [uniform_add_group F] [nontrivially_normed_field 𝕜] [module 𝕜 E] [module 𝕜 F] [has_continuous_smul 𝕜 E] {f : E →ₗ[𝕜] F} {h : ∃ (V : set E) (hV : V ∈ nhds 0), bornology.is_vonN_bounded 𝕜 (⇑f '' V)} {x : E} :

⇑(f.clm_of_exists_bounded_image h) x = ⇑f x

source

theorem linear_map.continuous_at_zero_of_locally_bounded {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [add_comm_group E] [uniform_space E] [uniform_add_group E] [add_comm_group F] [uniform_space F] [topological_space.first_countable_topology E] [is_R_or_C 𝕜] [module 𝕜 E] [has_continuous_smul 𝕜 E] [is_R_or_C 𝕜'] [module 𝕜' F] [has_continuous_smul 𝕜' F] {σ : 𝕜 →+* 𝕜'} (f : E →ₛₗ[σ] F) (hf : ∀ (s : set E), bornology.is_vonN_bounded 𝕜 s → bornology.is_vonN_bounded 𝕜' (⇑f '' s)) :

continuous_at ⇑f 0

source

theorem linear_map.continuous_of_locally_bounded {𝕜 : Type u_1} {𝕜' : Type u_2} {E : Type u_3} {F : Type u_4} [add_comm_group E] [uniform_space E] [uniform_add_group E] [add_comm_group F] [uniform_space F] [topological_space.first_countable_topology E] [is_R_or_C 𝕜] [module 𝕜 E] [has_continuous_smul 𝕜 E] [is_R_or_C 𝕜'] [module 𝕜' F] [has_continuous_smul 𝕜' F] {σ : 𝕜 →+* 𝕜'} [uniform_add_group F] (f : E →ₛₗ[σ] F) (hf : ∀ (s : set E), bornology.is_vonN_bounded 𝕜 s → bornology.is_vonN_bounded 𝕜' (⇑f '' s)) :

continuous ⇑f

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