# 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.toSeminormFamily form a neighborhood basis of 0 in the weak topology.
• LinearMap.toSeminormFamily.withSeminorms: the topology of a weak space is induced by the family of seminorms B.toSeminormFamily.
• WeakBilin.locallyConvexSpace: a space endowed with a weak topology is locally convex.

## References #

• [Bourbaki, Topological Vector Spaces][bourbaki1987]

## Tags #

weak dual, seminorm

def LinearMap.toSeminorm {𝕜 : Type u_1} {E : Type u_2} [] [] [Module 𝕜 E] (f : E →ₗ[𝕜] 𝕜) :
Seminorm 𝕜 E

Construct a seminorm from a linear form f : E →ₗ[𝕜] 𝕜 over a normed field 𝕜 by fun x => ‖f x‖

Equations
• f.toSeminorm = ().comp f
Instances For
theorem LinearMap.coe_toSeminorm {𝕜 : Type u_1} {E : Type u_2} [] [] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} :
f.toSeminorm = fun (x : E) => f x
@[simp]
theorem LinearMap.toSeminorm_apply {𝕜 : Type u_1} {E : Type u_2} [] [] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} {x : E} :
f.toSeminorm x = f x
theorem LinearMap.toSeminorm_ball_zero {𝕜 : Type u_1} {E : Type u_2} [] [] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} {r : } :
f.toSeminorm.ball 0 r = {x : E | f x < r}
theorem LinearMap.toSeminorm_comp {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [Module 𝕜 E] [] [Module 𝕜 F] (f : F →ₗ[𝕜] 𝕜) (g : E →ₗ[𝕜] F) :
f.toSeminorm.comp g = (f ∘ₗ g).toSeminorm
def LinearMap.toSeminormFamily {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [Module 𝕜 E] [] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :

Construct a family of seminorms from a bilinear form.

Equations
• B.toSeminormFamily y = (B.flip y).toSeminorm
Instances For
@[simp]
theorem LinearMap.toSeminormFamily_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [Module 𝕜 E] [] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {x : E} {y : F} :
(B.toSeminormFamily y) x = (B x) y
theorem LinearMap.hasBasis_weakBilin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [Module 𝕜 E] [] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
(nhds 0).HasBasis B.toSeminormFamily.basisSets id
theorem LinearMap.weakBilin_withSeminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [Module 𝕜 E] [] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
WithSeminorms B.toSeminormFamily
instance WeakBilin.locallyConvexSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [] [] [Module 𝕜 E] [] [Module 𝕜 F] [] [] [] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} :
Equations
• =