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
UniformOnFun.continuousSMul_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 #
ContinuousLinearMap.strongTopologyis the topology mentioned above for an arbitrary
ContinuousLinearMap.topologicalSpaceis the topology of bounded convergence. This is declared as an instance.
Main statements #
ContinuousLinearMap.strongTopology.continuousSMulshow that the strong topology makes
E →L[𝕜] Fa topological vector space, with the assumptions on
ContinuousLinearMap.continuousSMulregister these facts as instances for the special case of bounded convergence.
- [N. Bourbaki, Topological Vector Spaces][bourbaki1987]
- 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
ContinuousLinearMap.strongTopology. 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.
Pre-composition by a fixed continuous linear map as a continuous linear map. Note that in non-normed space it is not always true that composition is continuous in both variables, so we have to fix one of them.
Post-composition by a fixed continuous linear map as a continuous linear map. Note that in non-normed space it is not always true that composition is continuous in both variables, so we have to fix one of them.
A pair of continuous (semi)linear equivalences generates a (semi)linear equivalence between the spaces of continuous (semi)linear maps.
A pair of continuous linear equivalences generates a continuous linear equivalence between the spaces of continuous linear maps.