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 #

• continuous_linear_map.strong_topology is the topology mentioned above for an arbitrary 𝔖.
• continuous_linear_map.topological_space is the topology of bounded convergence. This is declared as an instance.

Main statements #

• continuous_linear_map.strong_topology.topological_add_group and continuous_linear_map.strong_topology.has_continuous_smul show that the strong topology makes E →L[𝕜] F a topological vector space, with the assumptions on 𝔖 mentioned above.
• continuous_linear_map.topological_add_group and continuous_linear_map.has_continuous_smul register these facts as instances for the special case of bounded convergence.

References #

• N. Bourbaki, Topological Vector Spaces

TODO #

• show that these topologies are T₂ and locally convex if the topology on F is
• add a type alias for continuous linear maps with the topology of 𝔖-convergence?

Tags #

uniform convergence, bounded convergence