mathlib3 documentation

analysis.locally_convex.weak_dual

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 #

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 →ₗ[𝕜] 𝕜} :
(f.to_seminorm) = λ (x : E), f x
@[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 →ₗ[𝕜] 𝕜) :

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