mathlib documentation

analysis.locally_convex.weak_dual

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 #

Main statements #

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
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 : ℝ} :
f.to_seminorm.ball 0 r = {x : E | βˆ₯⇑f xβˆ₯ < 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) :
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
@[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 β†’β‚—[π•œ] π•œ} :