Weak dual topology #
This file defines the weak topology given two vector spaces E
and F
over a commutative semiring
π
and a bilinear form B : E ββ[π] F ββ[π] π
. The weak topology on E
is the coarsest topology
such that for all y : F
every map Ξ» x, B x y
is continuous.
In the case that F = E βL[π] π
and B
being the canonical pairing, we obtain the weak-* topology,
weak_dual π E := (E βL[π] π)
. Interchanging the arguments in the bilinear form yields the
weak topology weak_space π E := E
.
Main definitions #
The main definitions are the types weak_bilin B
for the general case and the two special cases
weak_dual π E
and weak_space π E
with the respective topology instances on it.
- Given
B : E ββ[π] F ββ[π] π
, the typeweak_bilin B
is a type synonym forE
. - The instance
weak_bilin.topological_space
is the weak topology induced by the bilinear formB
. weak_dual π E
is a type synonym fordual π E
(when the latter is defined): both are equal to the typeE βL[π] π
of continuous linear maps from a moduleE
overπ
to the ringπ
.- The instance
weak_dual.topological_space
is the weak-* topology onweak_dual π E
, i.e., the coarsest topology making the evaluation maps at allz : E
continuous. weak_space π E
is a type synonym forE
(when the latter is defined).- The instance
weak_dual.topological_space
is the weak topology onE
, i.e., the coarsest topology such that allv : dual π E
remain continuous.
Main results #
We establish that weak_bilin B
has the following structure:
weak_bilin.has_continuous_add
: The addition inweak_bilin B
is continuous.weak_bilin.has_continuous_smul
: The scalar multiplication inweak_bilin B
is continuous.
We prove the following results characterizing the weak topology:
eval_continuous
: For anyy : F
, the evaluation mappingΞ» x, B x y
is continuous.continuous_of_continuous_eval
: For a mapping toweak_bilin B
to be continuous, it suffices that its compositions with pairing withB
at all pointsy : F
is continuous.tendsto_iff_forall_eval_tendsto
: Convergence inweak_bilin B
can be characterized in terms of convergence of the evaluations at all pointsy : F
.
Notations #
No new notation is introduced.
References #
Tags #
weak-star, weak dual, duality
The space E
equipped with the weak topology induced by the bilinear form B
.
Equations
- weak_bilin B = E
Equations
Equations
- weak_bilin.module' B = m
Equations
- weak_bilin.topological_space B = topological_space.induced (Ξ» (x : weak_bilin B) (y : F), β(βB x) y) Pi.topological_space
The coercion (Ξ» x y, B x y) : E β (F β π)
is continuous.
The coercion (Ξ» x y, B x y) : E β (F β π)
is an embedding.
Addition in weak_space B
is continuous.
Scalar multiplication by π
on weak_bilin B
is continuous.
weak_space B
is a topological_add_group
, meaning that addition and negation are
continuous.
The canonical pairing of a vector space and its topological dual.
Equations
- top_dual_pairing π E = continuous_linear_map.coe_lm π
The weak star topology is the topology coarsest topology on E βL[π] π
such that all
functionals Ξ» v, top_dual_pairing π E v x
are continuous.
Equations
- weak_dual π E = weak_bilin (top_dual_pairing π E)
Instances for weak_dual
- weak_dual.add_comm_monoid
- weak_dual.module
- weak_dual.topological_space
- weak_dual.has_continuous_add
- weak_dual.inhabited
- weak_dual.weak_dual.continuous_linear_map_class
- weak_dual.has_coe_to_fun
- weak_dual.mul_action
- weak_dual.distrib_mul_action
- weak_dual.module'
- weak_dual.has_continuous_const_smul
- weak_dual.has_continuous_smul
- weak_dual.t2_space
Helper instance for when there's too many metavariables to apply fun_like.has_coe_to_fun
directly.
Equations
If a monoid M
distributively continuously acts on π
and this action commutes with
multiplication on π
, then it acts on weak_dual π E
.
Equations
If a monoid M
distributively continuously acts on π
and this action commutes with
multiplication on π
, then it acts distributively on weak_dual π E
.
If π
is a topological module over a semiring R
and scalar multiplication commutes with the
multiplication on π
, then weak_dual π E
is a module over R
.
Equations
If a monoid M
distributively continuously acts on π
and this action commutes with
multiplication on π
, then it continuously acts on weak_dual π E
.
The weak topology is the topology coarsest topology on E
such that all
functionals Ξ» x, top_dual_pairing π E v x
are continuous.
Equations
- weak_space π E = weak_bilin (top_dual_pairing π E).flip
Instances for weak_space
A continuous linear map from E
to F
is still continuous when E
and F
are equipped with
their weak topologies.
Equations
- weak_space.map f = {to_linear_map := f.to_linear_map, cont := _}