mathlib documentation

analysis.seminorm

Seminorms and Local Convexity

This file introduces the following notions, defined for a vector space over a normed field:

We prove related properties.

TODO

Define and show equivalence of two notions of local convexity for a topological vector space over ℝ or ℂ: that it has a local base of balanced convex absorbent sets, and that it carries the initial topology induced by a family of seminorms.

References

Subset Properties

Absorbent and balanced sets in a vector space over a nondiscrete normed field.

def absorbs (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (A B : set E) :
Prop

A set A absorbs another set B if B is contained in scaling A by elements of sufficiently large norms.

Equations
def absorbent (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (A : set E) :
Prop

A set is absorbent if it absorbs every singleton.

Equations
def balanced (𝕜 : Type u_1) [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (A : set E) :
Prop

A set A is balanced if a • A is contained in A whenever a has norm no greater than one.

Equations
theorem balanced.absorbs_self {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] {A : set E} (hA : balanced 𝕜 A) :
absorbs 𝕜 A A

A balanced set absorbs itself.

Properties of balanced and absorbing sets in a topological vector space:

theorem absorbent_nhds_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] {A : set E} [topological_space E] [topological_vector_space 𝕜 E] (hA : A 𝓝 0) :
absorbent 𝕜 A

Every neighbourhood of the origin is absorbent.

theorem balanced_zero_union_interior {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] {A : set E} [topological_space E] [topological_vector_space 𝕜 E] (hA : balanced 𝕜 A) :
balanced 𝕜 ({0} interior A)

The union of {0} with the interior of a balanced set is balanced.

theorem balanced.interior {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] {A : set E} [topological_space E] [topological_vector_space 𝕜 E] (hA : balanced 𝕜 A) (h : 0 interior A) :

The interior of a balanced set is balanced if it contains the origin.

theorem balanced.closure {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] {A : set E} [topological_space E] [topological_vector_space 𝕜 E] (hA : balanced 𝕜 A) :
balanced 𝕜 (closure A)

The closure of a balanced set is balanced.

Seminorms

structure seminorm (𝕜 : Type u_1) (E : Type u_2) [normed_field 𝕜] [add_comm_group E] [vector_space 𝕜 E] :
Type u_2

A seminorm on a vector space over a normed field is a function to the reals that is positive semidefinite, positive homogeneous, and subadditive.

@[instance]
def seminorm.inhabited {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] :

Equations
@[instance]
def seminorm.has_coe_to_fun {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] :

Equations
theorem seminorm.smul {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (c : 𝕜) (x : E) :
p (c x) = c * p x

theorem seminorm.triangle {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p (x + y) p x + p y

@[simp]
theorem seminorm.zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) :
p 0 = 0

@[simp]
theorem seminorm.neg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (x : E) :
p (-x) = p x

theorem seminorm.nonneg {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (x : E) :
0 p x

theorem seminorm.sub_rev {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :
p (x - y) = p (y - x)

def seminorm.ball {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (x : E) (r : ) :
set E

The ball of radius r at x with respect to seminorm p is the set of elements y with p (y - x) <r`.

Equations
theorem seminorm.mem_ball {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (x y : E) (r : ) :
y p.ball x r p (y - x) < r

theorem seminorm.mem_ball_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (y : E) (r : ) :
y p.ball 0 r p y < r

theorem seminorm.ball_zero_eq {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (r : ) :
p.ball 0 r = {y : E | p y < r}

theorem seminorm.balanced_ball_zero {𝕜 : Type u_1} [nondiscrete_normed_field 𝕜] {E : Type u_2} [add_comm_group E] [vector_space 𝕜 E] (p : seminorm 𝕜 E) (r : ) :
balanced 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are balanced.