Seminorms and Local Convexity #

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

the subset properties of being absorbent and balanced,
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

Subset Properties #

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

source

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

absorbs 𝕜 A B = ∃ (r : ℝ) (H : r > 0), ∀ (a : 𝕜), r ≤ ∥a∥ → B ⊆ a • A

source

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

absorbent 𝕜 A = ∀ (x : E), ∃ (r : ℝ) (H : r > 0), ∀ (a : 𝕜), r ≤ ∥a∥ → x ∈ a • A

source

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

balanced 𝕜 A = ∀ (a : 𝕜), ∥a∥ ≤ 1 → a • A ⊆ A

source

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:

source

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] [has_continuous_smul 𝕜 E] (hA : A ∈ 𝓝 0) :

absorbent 𝕜 A

Every neighbourhood of the origin is absorbent.

source

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] [has_continuous_smul 𝕜 E] (hA : balanced 𝕜 A) :

balanced 𝕜 ({0} ∪ interior A)

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

source

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] [has_continuous_smul 𝕜 E] (hA : balanced 𝕜 A) (h : 0 ∈ interior A) :

balanced 𝕜 (interior A)

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

source

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] [has_continuous_smul 𝕜 E] (hA : balanced 𝕜 A) :

balanced 𝕜 (closure A)

The closure of a balanced set is balanced.

Seminorms #

source

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

Type u_2

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.

source

@[instance]

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

inhabited (seminorm 𝕜 E)

Equations

seminorm.inhabited = {default := {to_fun := λ (_x : E), 0, smul' := _, triangle' := _}}

source

@[instance]

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

has_coe_to_fun (seminorm 𝕜 E)

Equations

seminorm.has_coe_to_fun = {F := λ (p : seminorm 𝕜 E), E → ℝ, coe := λ (p : seminorm 𝕜 E), p.to_fun}

source

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

source

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

source

@[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

source

@[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

source

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

source

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)

source

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

p.ball x r = {y : E | ⇑p (y - x) < r}

source

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

source

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

source

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}

source

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.