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‖

Equations

• LinearMap.toSeminorm f = Seminorm.comp (normSeminorm 𝕜 𝕜) f

theorem LinearMap.coe_toSeminorm {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} : ⇑(LinearMap.toSeminorm f) = 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} : (LinearMap.toSeminorm f) x = ‖f x‖

theorem LinearMap.toSeminorm_ball_zero {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} {r : ℝ} : Seminorm.ball (LinearMap.toSeminorm f) 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) : Seminorm.comp (LinearMap.toSeminorm f) g = LinearMap.toSeminorm (f ∘ₗ g)

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.

Equations

• LinearMap.toSeminormFamily B y = LinearMap.toSeminorm ((LinearMap.flip B) y)

@[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} : (LinearMap.toSeminormFamily B y) x = ‖(B x) y‖

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 →ₗ[𝕜] 𝕜) : Filter.HasBasis (nhds 0) (SeminormFamily.basisSets (LinearMap.toSeminormFamily B)) id

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 (LinearMap.toSeminormFamily B)

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)

Equations

• (_ : LocallyConvexSpace ℝ (WeakBilin B)) = (_ : LocallyConvexSpace ℝ (WeakBilin B))