Local convexity #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines absorbent and balanced sets.
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.
Main declarations #
For a module over a normed ring:
absorbs: A setsabsorbs a settif all large scalings ofscontaint.absorbent: A setsis absorbent if every point eventually belongs to all large scalings ofs.balanced: A setsis balanced ifa • s ⊆ sfor allaof norm less than1.
References #
Tags #
absorbent, balanced, locally convex, LCTVS
@[simp]
theorem
absorbs_empty
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s : set E} :
theorem
absorbs.mono_left
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s t u : set E}
(hs : absorbs 𝕜 s u)
(h : s ⊆ t) :
absorbs 𝕜 t u
theorem
absorbs.mono_right
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s u v : set E}
(hs : absorbs 𝕜 s u)
(h : v ⊆ u) :
absorbs 𝕜 s v
theorem
absorbent.subset
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{A B : set E}
(hA : absorbent 𝕜 A)
(hAB : A ⊆ B) :
absorbent 𝕜 B
theorem
absorbent.absorbs
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s : set E}
(hs : absorbent 𝕜 s)
{x : E} :
absorbs 𝕜 s {x}
@[simp]
@[simp]
theorem
balanced.smul
{𝕜 : Type u_1}
{𝕝 : Type u_2}
{E : Type u_3}
[semi_normed_ring 𝕜]
[has_smul 𝕜 E]
{s : set E}
[has_smul 𝕝 E]
[smul_comm_class 𝕜 𝕝 E]
(a : 𝕝)
(hs : balanced 𝕜 s) :
theorem
absorbs.neg
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t : set E} :
theorem
balanced.neg
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E} :
theorem
absorbs.add
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s₁ s₂ t₁ t₂ : set E} :
theorem
balanced.add
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t : set E}
(hs : balanced 𝕜 s)
(ht : balanced 𝕜 t) :
theorem
absorbs.sub
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s₁ s₂ t₁ t₂ : set E}
(h₁ : absorbs 𝕜 s₁ t₁)
(h₂ : absorbs 𝕜 s₂ t₂) :
theorem
balanced.sub
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t : set E}
(hs : balanced 𝕜 s)
(ht : balanced 𝕜 t) :
theorem
balanced_zero
{𝕜 : Type u_1}
{E : Type u_3}
[semi_normed_ring 𝕜]
[add_comm_group E]
[module 𝕜 E] :
balanced 𝕜 0
theorem
balanced.smul_mono
{𝕜 : Type u_1}
{𝕝 : Type u_2}
{E : Type u_3}
[normed_field 𝕜]
[normed_ring 𝕝]
[normed_space 𝕜 𝕝]
[add_comm_group E]
[module 𝕜 E]
[smul_with_zero 𝕝 E]
[is_scalar_tower 𝕜 𝕝 E]
{s : set E}
(hs : balanced 𝕝 s)
{a : 𝕝}
{b : 𝕜}
(h : ‖a‖ ≤ ‖b‖) :
Scalar multiplication (by possibly different types) of a balanced set is monotone.
theorem
balanced.absorbs_self
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
(hA : balanced 𝕜 A) :
absorbs 𝕜 A A
A balanced set absorbs itself.
theorem
balanced.subset_smul
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
{a : 𝕜}
(hA : balanced 𝕜 A)
(ha : 1 ≤ ‖a‖) :
theorem
balanced.smul_eq
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
{a : 𝕜}
(hA : balanced 𝕜 A)
(ha : ‖a‖ = 1) :
theorem
balanced.neg_mem_iff
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
{x : E}
(hs : balanced 𝕜 s) :
theorem
absorbs.inter
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t u : set E}
(hs : absorbs 𝕜 s u)
(ht : absorbs 𝕜 t u) :
@[simp]
theorem
absorbs_inter
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s t u : set E} :
theorem
absorbent_univ
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E] :
theorem
absorbent_nhds_zero
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : A ∈ nhds 0) :
absorbent 𝕜 A
Every neighbourhood of the origin is absorbent.
theorem
balanced_zero_union_interior
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : balanced 𝕜 A) :
The union of {0} with the interior of a balanced set is balanced.
theorem
balanced.interior
{𝕜 : Type u_1}
{E : Type u_3}
[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) :
The interior of a balanced set is balanced if it contains the origin.
theorem
balanced.closure
{𝕜 : Type u_1}
{E : Type u_3}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{A : set E}
[topological_space E]
[has_continuous_smul 𝕜 E]
(hA : balanced 𝕜 A) :
theorem
absorbs_zero_iff
{𝕜 : Type u_1}
{E : Type u_3}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E} :
theorem
absorbent.zero_mem
{𝕜 : Type u_1}
{E : Type u_3}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
(hs : absorbent 𝕜 s) :
0 ∈ s
theorem
balanced_convex_hull_of_balanced
{𝕜 : Type u_1}
{E : Type u_3}
[nontrivially_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{s : set E}
[module ℝ E]
[smul_comm_class ℝ 𝕜 E]
(hs : balanced 𝕜 s) :
balanced 𝕜 (⇑(convex_hull ℝ) s)