Locally convex topological modules #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A locally_convex_space is a topological semimodule over an ordered semiring in which any point admits a neighborhood basis made of convex sets, or equivalently, in which convex neighborhoods of a point form a neighborhood basis at that point.

In a module, this is equivalent to 0 satisfying such properties.

Main results #

locally_convex_space_iff_zero : in a module, local convexity at zero gives local convexity everywhere
seminorm.locally_convex_space : a topology generated by a family of seminorms is locally convex
normed_space.locally_convex_space : a normed space is locally convex

TODO #

define a structure locally_convex_filter_basis, extending module_filter_basis, for filter bases generating a locally convex topology

source

@[class]

structure locally_convex_space (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

Prop

convex_basis : ∀ (x : E), (nhds x).has_basis (λ (s : set E), s ∈ nhds x ∧ convex 𝕜 s) id

A locally_convex_space is a topological semimodule over an ordered semiring in which convex neighborhoods of a point form a neighborhood basis at that point.

Instances of this typeclass

source

theorem locally_convex_space_iff (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

locally_convex_space 𝕜 E ↔ ∀ (x : E), (nhds x).has_basis (λ (s : set E), s ∈ nhds x ∧ convex 𝕜 s) id

source

theorem locally_convex_space.of_bases (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] {ι : Type u_3} (b : E → ι → set E) (p : E → ι → Prop) (hbasis : ∀ (x : E), (nhds x).has_basis (p x) (b x)) (hconvex : ∀ (x : E) (i : ι), p x i → convex 𝕜 (b x i)) :

locally_convex_space 𝕜 E

source

theorem locally_convex_space.convex_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] [locally_convex_space 𝕜 E] :

(nhds 0).has_basis (λ (s : set E), s ∈ nhds 0 ∧ convex 𝕜 s) id

source

theorem locally_convex_space_iff_exists_convex_subset (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [topological_space E] :

locally_convex_space 𝕜 E ↔ ∀ (x : E) (U : set E), U ∈ nhds x → (∃ (S : set E) (H : S ∈ nhds x), convex 𝕜 S ∧ S ⊆ U)

source

theorem locally_convex_space.of_basis_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] {ι : Type u_3} (b : ι → set E) (p : ι → Prop) (hbasis : (nhds 0).has_basis p b) (hconvex : ∀ (i : ι), p i → convex 𝕜 (b i)) :

locally_convex_space 𝕜 E

source

theorem locally_convex_space_iff_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] :

locally_convex_space 𝕜 E ↔ (nhds 0).has_basis (λ (s : set E), s ∈ nhds 0 ∧ convex 𝕜 s) id

source

theorem locally_convex_space_iff_exists_convex_subset_zero (𝕜 : Type u_1) (E : Type u_2) [ordered_semiring 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] :

locally_convex_space 𝕜 E ↔ ∀ (U : set E), U ∈ nhds 0 → (∃ (S : set E) (H : S ∈ nhds 0), convex 𝕜 S ∧ S ⊆ U)

source

@[protected, instance]

def locally_convex_space.to_locally_connected_space (E : Type u_2) [add_comm_group E] [topological_space E] [topological_add_group E] [module ℝ E] [has_continuous_smul ℝ E] [locally_convex_space ℝ E] :

locally_connected_space E

source

theorem locally_convex_space.convex_open_basis_zero (𝕜 : Type u_1) (E : Type u_2) [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] [locally_convex_space 𝕜 E] :

(nhds 0).has_basis (λ (s : set E), 0 ∈ s ∧ is_open s ∧ convex 𝕜 s) id

source

theorem disjoint.exists_open_convexes {𝕜 : Type u_1} {E : Type u_2} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] [locally_convex_space 𝕜 E] {s t : set E} (disj : disjoint s t) (hs₁ : convex 𝕜 s) (hs₂ : is_compact s) (ht₁ : convex 𝕜 t) (ht₂ : is_closed t) :

∃ (u v : set E), is_open u ∧ is_open v ∧ convex 𝕜 u ∧ convex 𝕜 v ∧ s ⊆ u ∧ t ⊆ v ∧ disjoint u v

In a locally convex space, if s, t are disjoint convex sets, s is compact and t is closed, then we can find open disjoint convex sets containing them.

source

theorem locally_convex_space_Inf {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {ts : set (topological_space E)} (h : ∀ (t : topological_space E), t ∈ ts → locally_convex_space 𝕜 E) :

locally_convex_space 𝕜 E

source

theorem locally_convex_space_infi {ι : Sort u_1} {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {ts' : ι → topological_space E} (h' : ∀ (i : ι), locally_convex_space 𝕜 E) :

locally_convex_space 𝕜 E

source

theorem locally_convex_space_inf {𝕜 : Type u_2} {E : Type u_3} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] {t₁ t₂ : topological_space E} (h₁ : locally_convex_space 𝕜 E) (h₂ : locally_convex_space 𝕜 E) :

locally_convex_space 𝕜 E

source

theorem locally_convex_space_induced {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] {t : topological_space F} [locally_convex_space 𝕜 F] (f : E →ₗ[𝕜] F) :

locally_convex_space 𝕜 E

source

@[protected, instance]

def pi.locally_convex_space {𝕜 : Type u_2} [ordered_semiring 𝕜] {ι : Type u_1} {X : ι → Type u_3} [Π (i : ι), add_comm_monoid (X i)] [Π (i : ι), topological_space (X i)] [Π (i : ι), module 𝕜 (X i)] [∀ (i : ι), locally_convex_space 𝕜 (X i)] :

locally_convex_space 𝕜 (Π (i : ι), X i)

source

@[protected, instance]

def prod.locally_convex_space {𝕜 : Type u_2} {E : Type u_3} {F : Type u_4} [ordered_semiring 𝕜] [add_comm_monoid E] [module 𝕜 E] [add_comm_monoid F] [module 𝕜 F] [topological_space E] [topological_space F] [locally_convex_space 𝕜 E] [locally_convex_space 𝕜 F] :

locally_convex_space 𝕜 (E × F)