Von Neumann Boundedness #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.bornology.is_vonN_bounded_iff_smul_tendsto_zero: Given any sequenceεof scalars which tends to𝓝[≠] 0, we have that a setSis bounded if and only if for any sequencex : ℕ → S,ε • xtends to 0. This shows that bounded sets are completely determined by sequences, which is the key fact for proving that sequential continuity implies continuity for linear maps defined on a bornological space
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₂) :
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) :
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.smul_tendsto_zero
{𝕜 : Type u_1}
{E : Type u_3}
{ι : Type u_6}
[normed_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
[topological_space E]
{S : set E}
{ε : ι → 𝕜}
{x : ι → E}
{l : filter ι}
(hS : bornology.is_vonN_bounded 𝕜 S)
(hxS : ∀ᶠ (n : ι) in l, x n ∈ S)
(hε : filter.tendsto ε l (nhds 0)) :
filter.tendsto (ε • x) l (nhds 0)
theorem
bornology.is_vonN_bounded_of_smul_tendsto_zero
{E : Type u_3}
{ι : Type u_6}
{𝕝 : Type u_7}
[nontrivially_normed_field 𝕝]
[add_comm_group E]
[module 𝕝 E]
[topological_space E]
[has_continuous_smul 𝕝 E]
{ε : ι → 𝕝}
{l : filter ι}
[l.ne_bot]
(hε : ∀ᶠ (n : ι) in l, ε n ≠ 0)
{S : set E}
(H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → filter.tendsto (ε • x) l (nhds 0)) :
theorem
bornology.is_vonN_bounded_iff_smul_tendsto_zero
{E : Type u_3}
{ι : Type u_6}
{𝕝 : Type u_7}
[nontrivially_normed_field 𝕝]
[add_comm_group E]
[module 𝕝 E]
[topological_space E]
[has_continuous_smul 𝕝 E]
{ε : ι → 𝕝}
{l : filter ι}
[l.ne_bot]
(hε : filter.tendsto ε l (nhds_within 0 {0}ᶜ))
{S : set E} :
bornology.is_vonN_bounded 𝕝 S ↔ ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → filter.tendsto (ε • x) l (nhds 0)
Given any sequence ε of scalars which tends to 𝓝[≠] 0, we have that a set S is bounded
if and only if for any sequence x : ℕ → S, ε • x tends to 0. This actually works for any
indexing type ι, but in the special case ι = ℕ we get the important fact that convergent
sequences fully characterize bounded sets.
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) :
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) :
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 : ℝ) :
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