Weak Dual in Topological Vector Spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 form f : E →ₗ[𝕜] 𝕜 into a seminorm λ x, ‖f x‖.
linear_map.to_seminorm_family: turn a bilinear form B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜 into a map F → seminorm 𝕜 E.

Main statements #

linear_map.has_basis_weak_bilin: the seminorm balls of B.to_seminorm_family form a neighborhood basis of 0 in the weak topology.
linear_map.to_seminorm_family.with_seminorms: the topology of a weak space is induced by the family of seminorm B.to_seminorm_family.
weak_bilin.locally_convex_space: a spaced endowed with a weak topology is locally convex.

References #

Bourbaki, Topological Vector Spaces

Tags #

weak dual, seminorm

source

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

source

theorem linear_map.coe_to_seminorm {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {f : E →ₗ[𝕜] 𝕜} :

⇑(f.to_seminorm) = λ (x : E), ‖⇑f x‖

source

@[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} :

⇑(f.to_seminorm) x = ‖⇑f x‖

source

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 : ℝ} :

f.to_seminorm.ball 0 r = {x : E | ‖⇑f x‖ < r}

source

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

source

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

source

@[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} :

⇑(B.to_seminorm_family y) x = ‖⇑(⇑B x) y‖

source

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 →ₗ[𝕜] 𝕜) :

(nhds 0).has_basis B.to_seminorm_family.basis_sets id

source

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 →ₗ[𝕜] 𝕜) :

with_seminorms B.to_seminorm_family

source

@[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 →ₗ[𝕜] 𝕜} :

locally_convex_space ℝ (weak_bilin B)