Von Neumann Boundedness #
This file defines natural or von Neumann bounded sets and proves elementary properties.
Main declarations #
bornology.is_vonN_bounded: A setsis von Neumann-bounded if every neighborhood of zero absorbss.bornology.vonN_bornology: The bornology made of the von Neumann-bounded sets.
Main results #
bornology.is_vonN_bounded.of_topological_space_le: A coarser topology admits more von Neumann-bounded sets.bornology.is_vonN_bounded.image: A continuous linear image of a bounded set is bounded.
References #
def
bornology.is_vonN_bounded
(π : Type u_1)
{E : Type u_3}
[semi_normed_ring π]
[has_smul π E]
[has_zero E]
[topological_space E]
(s : set E) :
Prop
A set s is von Neumann bounded if every neighborhood of 0 absorbs s.
@[simp]
theorem
bornology.is_vonN_bounded_empty
(π : Type u_1)
(E : Type u_3)
[semi_normed_ring π]
[has_smul π E]
[has_zero E]
[topological_space E] :
theorem
bornology.is_vonN_bounded_iff
{π : Type u_1}
{E : Type u_3}
[semi_normed_ring π]
[has_smul π E]
[has_zero E]
[topological_space E]
(s : set E) :
theorem
filter.has_basis.is_vonN_bounded_basis_iff
{π : Type u_1}
{E : Type u_3}
{ΞΉ : Type u_6}
[semi_normed_ring π]
[has_smul π E]
[has_zero E]
[topological_space E]
{q : ΞΉ β Prop}
{s : ΞΉ β set E}
{A : set E}
(h : (nhds 0).has_basis q s) :
bornology.is_vonN_bounded π A β β (i : ΞΉ), q i β absorbs π (s i) A
theorem
bornology.is_vonN_bounded.subset
{π : Type u_1}
{E : Type u_3}
[semi_normed_ring π]
[has_smul π E]
[has_zero E]
[topological_space E]
{sβ sβ : set E}
(h : sβ β sβ)
(hsβ : bornology.is_vonN_bounded π sβ) :
bornology.is_vonN_bounded π sβ
Subsets of bounded sets are bounded.
theorem
bornology.is_vonN_bounded.union
{π : Type u_1}
{E : Type u_3}
[semi_normed_ring π]
[has_smul π E]
[has_zero E]
[topological_space E]
{sβ sβ : set E}
(hsβ : bornology.is_vonN_bounded π sβ)
(hsβ : bornology.is_vonN_bounded π sβ) :
bornology.is_vonN_bounded π (sβ βͺ sβ)
The union of two bounded sets is bounded.
theorem
bornology.is_vonN_bounded.of_topological_space_le
{π : Type u_1}
{E : Type u_3}
[semi_normed_ring π]
[add_comm_group E]
[module π E]
{t t' : topological_space E}
(h : t β€ t')
{s : set E}
(hs : bornology.is_vonN_bounded π s) :
bornology.is_vonN_bounded π s
If a topology t' is coarser than t, then any set s that is bounded with respect to
t is bounded with respect to t'.
theorem
bornology.is_vonN_bounded.image
{E : Type u_3}
{F : Type u_5}
{πβ : Type u_7}
{πβ : Type u_8}
[normed_division_ring πβ]
[normed_division_ring πβ]
[add_comm_group E]
[module πβ E]
[add_comm_group F]
[module πβ F]
[topological_space E]
[topological_space F]
{Ο : πβ β+* πβ}
[ring_hom_surjective Ο]
[ring_hom_isometric Ο]
{s : set E}
(hs : bornology.is_vonN_bounded πβ s)
(f : E βSL[Ο] F) :
bornology.is_vonN_bounded πβ (βf '' s)
A continuous linear image of a bounded set is bounded.
theorem
bornology.is_vonN_bounded_singleton
{π : Type u_1}
{E : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[topological_space E]
[has_continuous_smul π E]
(x : E) :
bornology.is_vonN_bounded π {x}
Singletons are bounded.
theorem
bornology.is_vonN_bounded_covers
{π : Type u_1}
{E : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[topological_space E]
[has_continuous_smul π E] :
The union of all bounded set is the whole space.
@[reducible]
def
bornology.vonN_bornology
(π : Type u_1)
(E : Type u_3)
[normed_field π]
[add_comm_group E]
[module π E]
[topological_space E]
[has_continuous_smul π E] :
The von Neumann bornology defined by the von Neumann bounded sets.
Note that this is not registered as an instance, in order to avoid diamonds with the metric bornology.
Equations
@[simp]
theorem
bornology.is_bounded_iff_is_vonN_bounded
(π : Type u_1)
{E : Type u_3}
[normed_field π]
[add_comm_group E]
[module π E]
[topological_space E]
[has_continuous_smul π E]
{s : set E} :
theorem
totally_bounded.is_vonN_bounded
(π : Type u_1)
{E : Type u_3}
[nontrivially_normed_field π]
[add_comm_group E]
[module π E]
[uniform_space E]
[uniform_add_group E]
[has_continuous_smul π E]
{s : set E}
(hs : totally_bounded s) :
bornology.is_vonN_bounded π s
theorem
normed_space.is_vonN_bounded_ball
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
(r : β) :
bornology.is_vonN_bounded π (metric.ball 0 r)
theorem
normed_space.is_vonN_bounded_closed_ball
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
(r : β) :
bornology.is_vonN_bounded π (metric.closed_ball 0 r)
theorem
normed_space.is_vonN_bounded_iff
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
(s : set E) :
theorem
normed_space.is_vonN_bounded_iff'
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
(s : set E) :
theorem
normed_space.image_is_vonN_bounded_iff
(π : Type u_1)
(E : Type u_3)
{E' : Type u_4}
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
(f : E' β E)
(s : set E') :
theorem
normed_space.vonN_bornology_eq
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E] :
In a normed space, the von Neumann bornology (bornology.vonN_bornology) is equal to the
metric bornology.
theorem
normed_space.is_bounded_iff_subset_smul_ball
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
{s : set E} :
bornology.is_bounded s β β (a : π), s β a β’ metric.ball 0 1
theorem
normed_space.is_bounded_iff_subset_smul_closed_ball
(π : Type u_1)
(E : Type u_3)
[nontrivially_normed_field π]
[seminormed_add_comm_group E]
[normed_space π E]
{s : set E} :
bornology.is_bounded s β β (a : π), s β a β’ metric.closed_ball 0 1