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 fun x => B x y
is continuous.
Main definitions #
The main definition is the type WeakBilin B
.
- Given
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
, the typeWeakBilin B
is a type synonym forE
. - The instance
WeakBilin.instTopologicalSpace
is the weak topology induced by the bilinear formB
.
Main results #
We establish that WeakBilin B
has the following structure:
WeakBilin.instContinuousAdd
: The addition inWeakBilin B
is continuous.WeakBilin.instContinuousSMul
: The scalar multiplication inWeakBilin B
is continuous.
We prove the following results characterizing the weak topology:
eval_continuous
: For anyy : F
, the evaluation mappingfun x => B x y
is continuous.continuous_of_continuous_eval
: For a mapping toWeakBilin B
to be continuous, it suffices that its compositions with pairing withB
at all pointsy : F
is continuous.tendsto_iff_forall_eval_tendsto
: Convergence inWeakBilin 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
Equations
Equations
Equations
Equations
Equations
- ⋯ = s
Equations
- WeakBilin.instTopologicalSpace B = TopologicalSpace.induced (fun (x : WeakBilin B) (y : F) => (B x) y) Pi.topologicalSpace
The coercion (fun x y => B x y) : E → (F → 𝕜)
is continuous.
The coercion (fun x y => B x y) : E → (F → 𝕜)
is an embedding.
Addition in WeakBilin B
is continuous.
Equations
- ⋯ = ⋯
Scalar multiplication by 𝕜
on WeakBilin B
is continuous.
Equations
- ⋯ = ⋯
WeakBilin B
is a TopologicalAddGroup
, meaning that addition and negation are
continuous.
Equations
- ⋯ = ⋯