Seminorms and Local Convexity
This file introduces the following notions, defined for a vector space over a normed field:
a
seminorm
, a function to the reals that is positive-semidefinite, absolutely homogeneous, and subadditive.
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
- [H. H. Schaefer, Topological Vector Spaces][schaefer1966]
Subset Properties
Absorbent and balanced sets in a vector space over a nondiscrete normed field.
A set A
absorbs another set B
if B
is contained in scaling
A
by elements of sufficiently large norms.
A set is absorbent if it absorbs every singleton.
A set A
is balanced if a • A
is contained in A
whenever a
has norm no greater than one.
A balanced set absorbs itself.
Properties of balanced and absorbing sets in a topological vector space:
Every neighbourhood of the origin is absorbent.
The union of {0}
with the interior of a balanced set
is balanced.
The interior of a balanced set is balanced if it contains the origin.
The closure of a balanced set is balanced.
Seminorms
- to_fun : E → ℝ
- smul' : ∀ (a : 𝕜) (x : E), c.to_fun (a • x) = ∥a∥ * c.to_fun x
- triangle' : ∀ (x y : E), c.to_fun (x + y) ≤ c.to_fun x + c.to_fun y
A seminorm on a vector space over a normed field is a function to the reals that is positive semidefinite, positive homogeneous, and subadditive.
The ball of radius r
at x
with respect to seminorm p
is the set of elements y
with p (y - x) <
r`.
Seminorm-balls at the origin are balanced.