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 explicit give a neighborhood basis in terms of the family of seminorms Ξ» x, βB x yβ
for y : F
.
Main definitions #
linear_map.to_seminorm
: turn a linear formf : E ββ[π] π
into a seminormΞ» x, βf xβ
.linear_map.to_seminorm_family
: turn a bilinear formB : E ββ[π] F ββ[π] π
into a mapF β seminorm π E
.
Main statements #
linear_map.has_basis_weak_bilin
: the seminorm balls ofB.to_seminorm_family
form a neighborhood basis of0
in the weak topology.linear_map.to_seminorm_family.with_seminorms
: the topology of a weak space is induced by the family of seminormB.to_seminorm_family
.weak_bilin.locally_convex_space
: a spaced endowed with a weak topology is locally convex.
References #
Tags #
weak dual, seminorm
def
linear_map.to_seminorm
{π : Type u_1}
{E : Type u_2}
[normed_field π]
[add_comm_group E]
[module π E]
(f : E ββ[π] π) :
seminorm π E
Construct a seminorm from a linear form f : E ββ[π] π
over a normed field π
by
Ξ» x, βf xβ
Equations
- f.to_seminorm = (norm_seminorm π π).comp f
theorem
linear_map.coe_to_seminorm
{π : Type u_1}
{E : Type u_2}
[normed_field π]
[add_comm_group E]
[module π E]
{f : E ββ[π] π} :
@[simp]
theorem
linear_map.to_seminorm_apply
{π : Type u_1}
{E : Type u_2}
[normed_field π]
[add_comm_group E]
[module π E]
{f : E ββ[π] π}
{x : E} :
theorem
linear_map.to_seminorm_ball_zero
{π : Type u_1}
{E : Type u_2}
[normed_field π]
[add_comm_group E]
[module π E]
{f : E ββ[π] π}
{r : β} :
theorem
linear_map.to_seminorm_comp
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[add_comm_group F]
[module π F]
(f : F ββ[π] π)
(g : E ββ[π] F) :
f.to_seminorm.comp g = (f.comp g).to_seminorm
def
linear_map.to_seminorm_family
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[add_comm_group F]
[module π F]
(B : E ββ[π] F ββ[π] π) :
seminorm_family π E F
Construct a family of seminorms from a bilinear form.
Equations
- B.to_seminorm_family = Ξ» (y : F), (β(B.flip) y).to_seminorm
@[simp]
theorem
linear_map.to_seminorm_family_apply
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[add_comm_group F]
[module π F]
{B : E ββ[π] F ββ[π] π}
{x : E}
{y : F} :
theorem
linear_map.has_basis_weak_bilin
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[add_comm_group F]
[module π F]
(B : E ββ[π] F ββ[π] π) :
theorem
linear_map.weak_bilin_with_seminorms
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[add_comm_group F]
[module π F]
(B : E ββ[π] F ββ[π] π) :
@[protected, instance]
def
weak_bilin.locally_convex_space
{π : Type u_1}
{E : Type u_2}
{F : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[add_comm_group F]
[module π F]
[normed_space β π]
[module β E]
[is_scalar_tower β π E]
{B : E ββ[π] F ββ[π] π} :