mathlib documentation

topology.algebra.module.strong_topology

Strong topologies on the space of continuous linear maps #

In this file, we define the strong topologies on E β†’L[π•œ] F associated with a family 𝔖 : set (set E) to be the topology of uniform convergence on the elements of 𝔖 (also called the topology of 𝔖-convergence).

The lemma uniform_on_fun.has_continuous_smul_of_image_bounded tells us that this is a vector space topology if the continuous linear image of any element of 𝔖 is bounded (in the sense of bornology.is_vonN_bounded).

We then declare an instance for the case where 𝔖 is exactly the set of all bounded subsets of E, giving us the so-called "topology of uniform convergence on bounded sets" (or "topology of bounded convergence"), which coincides with the operator norm topology in the case of normed_spaces.

Other useful examples include the weak-* topology (when 𝔖 is the set of finite sets or the set of singletons) and the topology of compact convergence (when 𝔖 is the set of relatively compact sets).

Main definitions #

Main statements #

References #

TODO #

Tags #

uniform convergence, bounded convergence

def continuous_linear_map.strong_topology {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] (𝔖 : set (set E)) :

Given E and F two topological vector spaces and 𝔖 : set (set E), then strong_topology Οƒ F 𝔖 is the "topology of uniform convergence on the elements of 𝔖" on E β†’L[π•œ] F.

If the continuous linear image of any element of 𝔖 is bounded, this makes E β†’L[π•œ] F a topological vector space.

Equations
def continuous_linear_map.strong_uniformity {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] (𝔖 : set (set E)) :

The uniform structure associated with continuous_linear_map.strong_topology. We make sure that this has nice definitional properties.

Equations
@[simp]
theorem continuous_linear_map.strong_uniformity_topology_eq {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_uniformity.uniform_embedding_coe_fn {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_topology.embedding_coe_fn {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_uniformity.uniform_add_group {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_topology.topological_add_group {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] (𝔖 : set (set E)) :
theorem continuous_linear_map.strong_topology.t2_space {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] [t2_space F] (𝔖 : set (set E)) (h𝔖 : ⋃₀ 𝔖 = set.univ) :
theorem continuous_linear_map.strong_topology.has_continuous_smul {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [ring_hom_surjective Οƒ] [ring_hom_isometric Οƒ] [topological_space F] [topological_add_group F] [has_continuous_smul π•œβ‚‚ F] (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) (h𝔖₃ : βˆ€ (S : set E), S ∈ 𝔖 β†’ bornology.is_vonN_bounded π•œβ‚ S) :
has_continuous_smul π•œβ‚‚ (E β†’SL[Οƒ] F)
theorem continuous_linear_map.strong_topology.has_basis_nhds_zero_of_basis {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] {ΞΉ : Type u_4} (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) {p : ΞΉ β†’ Prop} {b : ΞΉ β†’ set F} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (Ξ» (Si : set E Γ— ΞΉ), Si.fst ∈ 𝔖 ∧ p Si.snd) (Ξ» (Si : set E Γ— ΞΉ), {f : E β†’SL[Οƒ] F | βˆ€ (x : E), x ∈ Si.fst β†’ ⇑f x ∈ b Si.snd})
theorem continuous_linear_map.strong_topology.has_basis_nhds_zero {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] (Οƒ : π•œβ‚ β†’+* π•œβ‚‚) {E : Type u_3} (F : Type u_5) [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] (𝔖 : set (set E)) (h𝔖₁ : 𝔖.nonempty) (h𝔖₂ : directed_on has_subset.subset 𝔖) :
(nhds 0).has_basis (Ξ» (SV : set E Γ— set F), SV.fst ∈ 𝔖 ∧ SV.snd ∈ nhds 0) (Ξ» (SV : set E Γ— set F), {f : E β†’SL[Οƒ] F | βˆ€ (x : E), x ∈ SV.fst β†’ ⇑f x ∈ SV.snd})
@[protected, instance]
def continuous_linear_map.topological_space {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] :

The topology of bounded convergence on E β†’L[π•œ] F. This coincides with the topology induced by the operator norm when E and F are normed spaces.

Equations
@[protected, instance]
def continuous_linear_map.topological_add_group {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] :
@[protected, instance]
def continuous_linear_map.has_continuous_smul {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [ring_hom_surjective Οƒ] [ring_hom_isometric Οƒ] [topological_space F] [topological_add_group F] [has_continuous_smul π•œβ‚‚ F] :
has_continuous_smul π•œβ‚‚ (E β†’SL[Οƒ] F)
@[protected, instance]
def continuous_linear_map.uniform_space {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] :
Equations
@[protected, instance]
def continuous_linear_map.uniform_add_group {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [uniform_space F] [uniform_add_group F] :
@[protected, instance]
def continuous_linear_map.t2_space {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] [has_continuous_smul π•œβ‚ E] [t2_space F] :
@[protected]
theorem continuous_linear_map.has_basis_nhds_zero_of_basis {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] {ΞΉ : Type u_4} {p : ΞΉ β†’ Prop} {b : ΞΉ β†’ set F} (h : (nhds 0).has_basis p b) :
(nhds 0).has_basis (Ξ» (Si : set E Γ— ΞΉ), bornology.is_vonN_bounded π•œβ‚ Si.fst ∧ p Si.snd) (Ξ» (Si : set E Γ— ΞΉ), {f : E β†’SL[Οƒ] F | βˆ€ (x : E), x ∈ Si.fst β†’ ⇑f x ∈ b Si.snd})
@[protected]
theorem continuous_linear_map.has_basis_nhds_zero {π•œβ‚ : Type u_1} {π•œβ‚‚ : Type u_2} [normed_field π•œβ‚] [normed_field π•œβ‚‚] {Οƒ : π•œβ‚ β†’+* π•œβ‚‚} {E : Type u_3} {F : Type u_5} [add_comm_group E] [module π•œβ‚ E] [add_comm_group F] [module π•œβ‚‚ F] [topological_space E] [topological_space F] [topological_add_group F] :
(nhds 0).has_basis (Ξ» (SV : set E Γ— set F), bornology.is_vonN_bounded π•œβ‚ SV.fst ∧ SV.snd ∈ nhds 0) (Ξ» (SV : set E Γ— set F), {f : E β†’SL[Οƒ] F | βˆ€ (x : E), x ∈ SV.fst β†’ ⇑f x ∈ SV.snd})