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_space
s.
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
andcontinuous_linear_map.strong_topology.has_continuous_smul
show that the strong topology makesE βL[π] F
a topological vector space, with the assumptions onπ
mentioned above.continuous_linear_map.topological_add_group
andcontinuous_linear_map.has_continuous_smul
register these facts as instances for the special case of bounded convergence.
References #
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
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
The uniform structure associated with continuous_linear_map.strong_topology
. We make sure
that this has nice definitional properties.
Equations
- continuous_linear_map.strong_uniformity Ο F π = (uniform_space.comap coe_fn (uniform_on_fun.uniform_space E F π)).replace_topology _
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
- continuous_linear_map.topological_space = continuous_linear_map.strong_topology Ο F {S : set E | bornology.is_vonN_bounded πβ S}
Equations
- continuous_linear_map.uniform_space = continuous_linear_map.strong_uniformity Ο F {S : set E | bornology.is_vonN_bounded πβ S}