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
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
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
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
Main definitions #
continuous_linear_map.strong_topologyis the topology mentioned above for an arbitrary
continuous_linear_map.topological_spaceis the topology of bounded convergence. This is declared as an instance.
Main statements #
continuous_linear_map.strong_topology.has_continuous_smulshow that the strong topology makes
E →L[𝕜] Fa topological vector space, with the assumptions on
continuous_linear_map.has_continuous_smulregister these facts as instances for the special case of bounded convergence.
- show that these topologies are T₂ and locally convex if the topology on
- add a type alias for continuous linear maps with the topology of
uniform convergence, bounded convergence
If the continuous linear image of any element of
𝔖 is bounded, this makes
E →L[𝕜] F a
topological vector space.
The uniform structure associated with
continuous_linear_map.strong_topology. We make sure
that this has nice definitional properties.
The topology of bounded convergence on
E →L[𝕜] F. This coincides with the topology induced by
the operator norm when
F are normed spaces.