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.
• LinearMap.rightDualEquiv: When B is right-separating, F is linearly equivalent to the strong dual of E with the weak topology.
• LinearMap.leftDualEquiv: When B is left-separating, E is linearly equivalent to the strong dual of F with the weak topology.

References

• [Bourbaki, Topological Vector Spaces][bourbaki1987]
• [Rudin, Functional Analysis][rudin1991]

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

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

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.

Equations

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

@[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.dualEmbedding_injective_of_separatingRight {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (hr : B.SeparatingRight) : Function.Injective ⇑(WeakBilin.eval B)

theorem LinearMap.mem_span_iff_continuous_of_finite {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [Finite ι] [Field 𝕜] [t𝕜 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [T0Space 𝕜] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) : φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous ⇑φ

A linear functional φ can be expressed as a linear combination of linear functionals f₁,…,fₙ if and only if φ is continuous with respect to the topology induced by f₁,…,fₙ. See LinearMap.mem_span_iff_continuous for a result about arbitrary collections of linear functionals.

theorem LinearMap.mem_span_iff_continuous {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) : φ ∈ Submodule.span 𝕜 (Set.range f) ↔ Continuous ⇑φ

A linear functional φ is in the span of a collection of linear functionals if and only if φ is continuous with respect to the topology induced by the collection of linear functionals. See LinearMap.mem_span_iff_continuous_of_finite for a result about finite collections of linear functionals.

theorem LinearMap.mem_span_iff_bound {ι : Type u_4} {𝕜 : Type u_5} {E : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {f : ι → E →ₗ[𝕜] 𝕜} (φ : E →ₗ[𝕜] 𝕜) : φ ∈ Submodule.span 𝕜 (Set.range f) ↔ ∃ (s : Finset ι) (c : NNReal), φ.toSeminorm ≤ c • s.sup fun (i : ι) => (f i).toSeminorm

theorem LinearMap.dualEmbedding_surjective {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) : Function.Surjective ⇑(WeakBilin.eval B)

The Weak Representation Theorem: Every continuous functional on E endowed with the σ(E, F; B)-topology is of the form x ↦ B(x, y) for some y : F.

noncomputable def LinearMap.rightDualEquiv {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (hr : B.SeparatingRight) : F ≃ₗ[𝕜] StrongDual 𝕜 (WeakBilin B)

When B is right-separating, F is linearly equivalent to the strong dual of E with the weak topology.

Equations

• B.rightDualEquiv hr = LinearEquiv.ofBijective (WeakBilin.eval B) ⋯

noncomputable def LinearMap.leftDualEquiv {𝕜 : Type u_5} {E : Type u_6} {F : Type u_7} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [AddCommGroup F] [Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (hl : B.SeparatingLeft) : E ≃ₗ[𝕜] StrongDual 𝕜 (WeakBilin B.flip)

When B is left-separating, E is linearly equivalent to the strong dual of F with the weak topology.

Equations

• B.leftDualEquiv hl = B.flip.rightDualEquiv ⋯

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 (fun (x : Set E) => x ∈ 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)