# mathlib3documentation

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 #

• 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.

## Tags #

weak dual, seminorm

def linear_map.to_seminorm {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ E] (f : E →ₗ[𝕜] 𝕜) :
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 𝕜] [ 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 𝕜] [ E] {f : E →ₗ[𝕜] 𝕜} {x : E} :
theorem linear_map.to_seminorm_ball_zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [ 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 𝕜] [ E] [ 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 𝕜] [ E] [ F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
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 𝕜] [ E] [ 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 𝕜] [ E] [ F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) :
theorem linear_map.weak_bilin_with_seminorms {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [normed_field 𝕜] [ E] [ 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 𝕜] [ E] [ F] [ 𝕜] [ E] [ E] {B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜} :