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 formf : E →ₗ[𝕜] 𝕜
into a seminormfun x => ‖f x‖
.LinearMap.toSeminormFamily
: turn a bilinear formB : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
into a mapF → Seminorm 𝕜 E
.
Main statements #
LinearMap.hasBasis_weakBilin
: the seminorm balls ofB.toSeminormFamily
form a neighborhood basis of0
in the weak topology.LinearMap.toSeminormFamily.withSeminorms
: the topology of a weak space is induced by the family of seminormsB.toSeminormFamily
.WeakBilin.locallyConvexSpace
: a space endowed with a weak topology is locally convex.
References #
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
Instances For
theorem
LinearMap.coe_toSeminorm
{𝕜 : Type u_1}
{E : Type u_2}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
{f : E →ₗ[𝕜] 𝕜}
:
@[simp]
theorem
LinearMap.toSeminorm_apply
{𝕜 : Type u_1}
{E : Type u_2}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
{f : E →ₗ[𝕜] 𝕜}
{x : E}
:
theorem
LinearMap.toSeminorm_ball_zero
{𝕜 : Type u_1}
{E : Type u_2}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
{f : E →ₗ[𝕜] 𝕜}
{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
Instances For
@[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}
:
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 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 B.toSeminormFamily
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 →ₗ[𝕜] 𝕜}
:
Equations
- ⋯ = ⋯