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.
References #
def
bornology.is_vonN_bounded
(𝕜 : Type u_1)
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_scalar 𝕜 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_2)
[semi_normed_ring 𝕜]
[has_scalar 𝕜 E]
[has_zero E]
[topological_space E] :
theorem
bornology.is_vonN_bounded_iff
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_scalar 𝕜 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_2}
{ι : Type u_3}
[semi_normed_ring 𝕜]
[has_scalar 𝕜 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_2}
[semi_normed_ring 𝕜]
[has_scalar 𝕜 E]
[has_zero E]
[topological_space E]
{s₁ s₂ : set E}
(h : s₁ ⊆ s₂)
(hs₂ : bornology.is_vonN_bounded 𝕜 s₂) :
Subsets of bounded sets are bounded.
theorem
bornology.is_vonN_bounded.union
{𝕜 : Type u_1}
{E : Type u_2}
[semi_normed_ring 𝕜]
[has_scalar 𝕜 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_2}
[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) :
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_2}
{𝕜₁ : Type u_4}
{𝕜₂ : Type u_5}
{F : Type u_6}
[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_2}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[topological_space E]
[has_continuous_smul 𝕜 E]
(x : E) :
Singletons are bounded.
theorem
bornology.is_vonN_bounded_covers
{𝕜 : Type u_1}
{E : Type u_2}
[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.
def
bornology.vonN_bornology
(𝕜 : Type u_1)
(E : Type u_2)
[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_2}
[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_2}
[nondiscrete_normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[uniform_space E]
[uniform_add_group E]
[has_continuous_smul 𝕜 E]
[regular_space E]
{s : set E}
(hs : totally_bounded s) :