mathlib documentation

analysis.seminorm

Seminorms and Local Convexity #

This file defines absorbent sets, balanced sets, seminorms and the Minkowski functional.

An absorbent set is one that "surrounds" the origin. The idea is made precise by requiring that any point belongs to all large enough scalings of the set. This is the vector world analog of a topological neighborhood of the origin.

A balanced set is one that is everywhere around the origin. This means that a • s ⊆ s for all a of norm less than 1.

A seminorm is a function to the reals which is positive-semidefinite, absolutely homogeneous, and subadditive. They are closely related to convex sets and a topological vector space is locally convex if and only if its topology is induced by a family of seminorms.

The Minkowski functional of a set s is the function which associates each point to how much you need to scale s for x to be inside it. When s is symmetric, convex and absorbent, its gauge is a seminorm. Reciprocally, any seminorm arises as the gauge of some set, namely its unit ball. This induces the equivalence of seminorms and locally convex topological vector spaces.

Main declarations #

For a vector space over a normed field:

absorbent: A set s is absorbent if every point eventually belongs to all large scalings of s.
balanced: A set s is balanced if a • s ⊆ s for all a of norm less than 1.
seminorm: A function to the reals that is positive-semidefinite, absolutely homogeneous, and subadditive.
gauge: Aka Minkowksi functional. gauge s x is the least (actually, an infimum) r such that x ∈ r • s.
gauge_seminorm: The Minkowski functional as a seminorm, when s is symmetric, convex and absorbent.

References #

H. H. Schaefer, Topological Vector Spaces

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.

Prove the properties of balanced and absorbent sets of a real vector space.

Tags #

absorbent, balanced, seminorm, Minkowski functional, gauge, locally convex, LCTVS

Set Properties #

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

def absorbs (𝕜 : Type u_1) {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (A B : set E) :

Prop

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

Equations

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

def absorbent (𝕜 : Type u_1) {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (A : set E) :

Prop

A set is absorbent if it absorbs every singleton.

Equations

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

def balanced (𝕜 : Type u_1) {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (A : set E) :

Prop

A set A is balanced if a • A is contained in A whenever a has norm less than or equal to one.

Equations

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

theorem balanced.absorbs_self {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A : set E} (hA : balanced 𝕜 A) :

absorbs 𝕜 A A

A balanced set absorbs itself.

theorem balanced.univ {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] :

balanced 𝕜 set.univ

theorem balanced.union {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A₁ A₂ : set E} (hA₁ : balanced 𝕜 A₁) (hA₂ : balanced 𝕜 A₂) :

balanced 𝕜 (A₁ ∪ A₂)

theorem balanced.inter {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A₁ A₂ : set E} (hA₁ : balanced 𝕜 A₁) (hA₂ : balanced 𝕜 A₂) :

balanced 𝕜 (A₁ ∩ A₂)

theorem balanced.add {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A₁ A₂ : set E} (hA₁ : balanced 𝕜 A₁) (hA₂ : balanced 𝕜 A₂) :

balanced 𝕜 (A₁ + A₂)

theorem balanced.smul {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (a : 𝕜) {A : set E} (hA : balanced 𝕜 A) :

balanced 𝕜 (a • A)

theorem balanced.subset_smul {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A : set E} (hA : balanced 𝕜 A) {a : 𝕜} (ha : 1 ≤ ∥a∥) :

A ⊆ a • A

theorem balanced.smul_eq {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A : set E} (hA : balanced 𝕜 A) {a : 𝕜} (ha : ∥a∥ = 1) :

a • A = A

theorem absorbent.subset {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A B : set E} (hA : absorbent 𝕜 A) (hAB : A ⊆ B) :

absorbent 𝕜 B

theorem absorbent_iff_forall_absorbs_singleton {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A : set E} :

absorbent 𝕜 A ↔ ∀ (x : E), absorbs 𝕜 A {x}

theorem absorbent_iff_nonneg_lt {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A : set E} :

absorbent 𝕜 A ↔ ∀ (x : E), ∃ (r : ℝ), 0 ≤ r ∧ ∀ (a : 𝕜), r < ∥a∥ → x ∈ a • A

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

theorem absorbent_nhds_zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {A : set E} [topological_space E] [has_continuous_smul 𝕜 E] (hA : A ∈ 𝓝 0) :

absorbent 𝕜 A

Every neighbourhood of the origin is absorbent.

theorem balanced_zero_union_interior {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 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.

theorem balanced.interior {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 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.

theorem balanced.closure {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 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 #

structure seminorm (𝕜 : Type u_3) (E : Type u_4) [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] :

Type u_4

to_fun : E → ℝ
smul' : ∀ (a : 𝕜) (x : E), self.to_fun (a • x) = ∥a∥ * self.to_fun x
triangle' : ∀ (x y : E), self.to_fun (x + y) ≤ self.to_fun x + self.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.

@[protected, instance]

def seminorm.inhabited {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] :

inhabited (seminorm 𝕜 E)

Equations

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

@[protected, instance]

def seminorm.has_coe_to_fun {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] :

has_coe_to_fun (seminorm 𝕜 E) (λ (_x : seminorm 𝕜 E), E → ℝ)

Equations

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

@[ext]

theorem seminorm.ext {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] {p q : seminorm 𝕜 E} (h : ⇑p = ⇑q) :

p = q

@[protected]

theorem seminorm.smul {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (c : 𝕜) (x : E) :

⇑p (c • x) = ∥c∥ * ⇑p x

@[protected]

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

⇑p (x + y) ≤ ⇑p x + ⇑p y

@[protected]

theorem seminorm.sub_le {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :

⇑p (x - y) ≤ ⇑p x + ⇑p y

@[protected, simp]

theorem seminorm.zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) :

⇑p 0 = 0

@[protected, simp]

theorem seminorm.neg {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x : E) :

⇑p (-x) = ⇑p x

theorem seminorm.nonneg {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x : E) :

0 ≤ ⇑p x

theorem seminorm.sub_rev {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x y : E) :

⇑p (x - y) = ⇑p (y - x)

def seminorm.ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x : E) (r : ℝ) :

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}

theorem seminorm.mem_ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 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} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (y : E) (r : ℝ) :

y ∈ p.ball 0 r ↔ ⇑p y < r

theorem seminorm.ball_zero_eq {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (r : ℝ) :

p.ball 0 r = {y : E | ⇑p y < r}

theorem seminorm.balanced_ball_zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (r : ℝ) :

balanced 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are balanced.

theorem seminorm.absorbent_ball_zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) {r : ℝ} (hr : 0 < r) :

absorbent 𝕜 (p.ball 0 r)

Seminorm-balls at the origin are absorbent.

theorem seminorm.absorbent_ball {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (x : E) (r : ℝ) (hpr : ⇑p x < r) :

absorbent 𝕜 (p.ball x r)

Seminorm-balls containing the origin are absorbent.

theorem seminorm.symmetric_ball_zero {𝕜 : Type u_1} {E : Type u_2} [normed_field 𝕜] [add_comm_group E] [module 𝕜 E] (p : seminorm 𝕜 E) (r : ℝ) {x : E} (hx : x ∈ p.ball 0 r) :

-x ∈ p.ball 0 r

@[protected]

theorem seminorm.convex_on {𝕜 : Type u_1} {E : Type u_2} [normed_linear_ordered_field 𝕜] [add_comm_group E] [semi_normed_space ℝ 𝕜] [module 𝕜 E] [has_scalar ℝ E] [is_scalar_tower ℝ 𝕜 E] (p : seminorm 𝕜 E) :

convex_on ℝ set.univ ⇑p

A seminorm is convex. Also see convex_on_norm.

theorem seminorm.convex_ball {𝕜 : Type u_1} {E : Type u_2} [normed_linear_ordered_field 𝕜] [add_comm_group E] [semi_normed_space ℝ 𝕜] [module 𝕜 E] [module ℝ E] [is_scalar_tower ℝ 𝕜 E] (p : seminorm 𝕜 E) (x : E) (r : ℝ) :

convex ℝ (p.ball x r)

Seminorm-balls are convex.

noncomputable def gauge {E : Type u_2} [add_comm_group E] [module ℝ E] (s : set E) (x : E) :

The Minkowski functional. Given a set s in a real vector space, gauge s is the functional which sends x : E to the smallest r : ℝ such that x is in s scaled by r.

Equations

gauge s x = Inf {r : ℝ | 0 < r ∧ x ∈ r • s}

theorem gauge_def {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {x : E} :

gauge s x = Inf {r ∈ set.Ioi 0 | x ∈ r • s}

theorem gauge_def' {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {x : E} :

gauge s x = Inf {r ∈ set.Ioi 0 | r⁻¹ • x ∈ s}

An alternative definition of the gauge using scalar multiplication on the element rather than on the set.

theorem absorbent.gauge_set_nonempty {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {x : E} (absorbs : absorbent ℝ s) :

{r : ℝ | 0 < r ∧ x ∈ r • s}.nonempty

If the given subset is absorbent then the set we take an infimum over in gauge is nonempty, which is useful for proving many properties about the gauge.

theorem exists_lt_of_gauge_lt {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (absorbs : absorbent ℝ s) {x : E} {a : ℝ} (h : gauge s x < a) :

∃ (b : ℝ), 0 < b ∧ b < a ∧ x ∈ b • s

@[simp]

theorem gauge_zero {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} :

gauge s 0 = 0

The gauge evaluated at 0 is always zero (mathematically this requires 0 to be in the set s but, the real infimum of the empty set in Lean being defined as 0, it holds unconditionally).

theorem gauge_nonneg {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (x : E) :

0 ≤ gauge s x

The gauge is always nonnegative.

theorem gauge_neg {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (symmetric : ∀ (x : E), x ∈ s → -x ∈ s) (x : E) :

gauge s (-x) = gauge s x

theorem gauge_le_of_mem {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {r : ℝ} (hr : 0 ≤ r) {x : E} (hx : x ∈ r • s) :

gauge s x ≤ r

theorem gauge_le_one_eq' {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex ℝ s) (zero_mem : 0 ∈ s) (absorbs : absorbent ℝ s) :

{x : E | gauge s x ≤ 1} = ⋂ (r : ℝ) (H : 1 < r), r • s

theorem gauge_le_one_eq {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex ℝ s) (zero_mem : 0 ∈ s) (absorbs : absorbent ℝ s) :

{x : E | gauge s x ≤ 1} = ⋂ (r : ℝ) (H : r ∈ set.Ioi 1), r • s

theorem gauge_lt_one_eq' {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (absorbs : absorbent ℝ s) :

{x : E | gauge s x < 1} = ⋃ (r : ℝ) (H : 0 < r) (H : r < 1), r • s

theorem gauge_lt_one_eq {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (absorbs : absorbent ℝ s) :

{x : E | gauge s x < 1} = ⋃ (r : ℝ) (H : r ∈ set.Ioo 0 1), r • s

theorem gauge_lt_one_subset_self {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex ℝ s) (h₀ : 0 ∈ s) (absorbs : absorbent ℝ s) :

{x : E | gauge s x < 1} ⊆ s

theorem gauge_le_one_of_mem {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} {x : E} (hx : x ∈ s) :

gauge s x ≤ 1

theorem self_subset_gauge_le_one {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} :

s ⊆ {x : E | gauge s x ≤ 1}

theorem convex.gauge_le_one {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex ℝ s) (h₀ : 0 ∈ s) (absorbs : absorbent ℝ s) :

convex ℝ {x : E | gauge s x ≤ 1}

theorem interior_subset_gauge_lt_one {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [has_continuous_smul ℝ E] (s : set E) :

interior s ⊆ {x : E | gauge s x < 1}

theorem gauge_lt_one_eq_self_of_open {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) (zero_mem : 0 ∈ s) (hs₂ : is_open s) :

{x : E | gauge s x < 1} = s

theorem gauge_lt_one_of_mem_of_open {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) (zero_mem : 0 ∈ s) (hs₂ : is_open s) (x : E) (hx : x ∈ s) :

gauge s x < 1

theorem one_le_gauge_of_not_mem {E : Type u_2} [add_comm_group E] [module ℝ E] [topological_space E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) (zero_mem : 0 ∈ s) (hs₂ : is_open s) {x : E} (hx : x ∉ s) :

1 ≤ gauge s x

theorem gauge_smul_of_nonneg {E : Type u_2} [add_comm_group E] [module ℝ E] {α : Type u_3} [linear_ordered_field α] [mul_action_with_zero α ℝ] [ordered_smul α ℝ] [mul_action_with_zero α E] [is_scalar_tower α ℝ (set E)] {s : set E} {r : α} (hr : 0 ≤ r) (x : E) :

gauge s (r • x) = r • gauge s x

theorem gauge_smul {E : Type u_2} [add_comm_group E] [module ℝ E] {α : Type u_3} [linear_ordered_field α] [mul_action_with_zero α ℝ] [ordered_smul α ℝ] [module α E] [is_scalar_tower α ℝ (set E)] {s : set E} (symmetric : ∀ (x : E), x ∈ s → -x ∈ s) (r : α) (x : E) :

gauge s (r • x) = |r| • gauge s x

In textbooks, this is the homogeneity of the Minkowksi functional.

theorem gauge_add_le {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (hs : convex ℝ s) (absorbs : absorbent ℝ s) (x y : E) :

gauge s (x + y) ≤ gauge s x + gauge s y

noncomputable def gauge_seminorm {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (symmetric : ∀ (x : E), x ∈ s → -x ∈ s) (hs : convex ℝ s) (hs' : absorbent ℝ s) :

gauge s as a seminorm when s is symmetric, convex and absorbent.

Equations

gauge_seminorm symmetric hs hs' = {to_fun := gauge s, smul' := _, triangle' := _}

@[simp]

theorem gauge_seminorm_to_fun {E : Type u_2} [add_comm_group E] [module ℝ E] {s : set E} (symmetric : ∀ (x : E), x ∈ s → -x ∈ s) (hs : convex ℝ s) (hs' : absorbent ℝ s) (x : E) :

⇑(gauge_seminorm symmetric hs hs') x = gauge s x

theorem seminorm.gauge_ball {E : Type u_2} [add_comm_group E] [module ℝ E] (p : seminorm ℝ E) :

gauge (p.ball 0 1) = ⇑p

Any seminorm arises a the gauge of its unit ball.

theorem seminorm.gauge_seminorm_ball {E : Type u_2} [add_comm_group E] [module ℝ E] (p : seminorm ℝ E) :

gauge_seminorm _ _ _ = p