Weak Dual in Topological Vector Spaces #
We prove that the weak topology induced by a bilinear form
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 is locally
convex and we explicitly give a neighborhood basis in terms of the family of seminorms
fun x => ‖B x y‖ for
y : F.
Main definitions #
LinearMap.toSeminorm: turn a linear form
f : E →ₗ[𝕜] 𝕜into a seminorm
fun x => ‖f x‖.
LinearMap.toSeminormFamily: turn a bilinear form
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜into a map
F → Seminorm 𝕜 E.
Main statements #
LinearMap.hasBasis_weakBilin: the seminorm balls of
B.toSeminormFamilyform a neighborhood basis of
0in the weak topology.
LinearMap.toSeminormFamily.withSeminorms: the topology of a weak space is induced by the family of seminorms
WeakBilin.locallyConvexSpace: a space endowed with a weak topology is locally convex.
- [Bourbaki, Topological Vector Spaces][bourbaki1987]
weak dual, seminorm