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} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] (f : E →ₗ[𝕜] 𝕜) : Seminorm 𝕜 E

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

theorem LinearMap.coe_toSeminorm {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} : ⇑f.toSeminorm = fun (x : E) => ‖f x‖

@[simp]

theorem LinearMap.toSeminorm_apply {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} {x : E} : f.toSeminorm x = ‖f x‖

theorem LinearMap.toSeminorm_ball_zero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [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} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [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} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : SeminormFamily 𝕜 E F

Construct a family of seminorms from a bilinear form.

@[simp]

theorem LinearMap.toSeminormFamily_apply {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} {x : E} {y : F} : (B.toSeminormFamily y) x = ‖(B x) y‖

theorem LinearMap.weakBilin_withSeminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : WithSeminorms B.toSeminormFamily

theorem LinearMap.hasBasis_weakBilin {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : (nhds 0).HasBasis B.toSeminormFamily.basisSets _root_.id

instance WeakBilin.locallyConvexSpace {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} : LocallyConvexSpace ℝ (WeakBilin B)