# mathlib3documentation

analysis.locally_convex.bounded

# 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 set s is von Neumann-bounded if every neighborhood of zero absorbs s.
• 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 set S is bounded if and only if for any sequence x : ℕ → S, ε • x tends 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} [ E] [has_zero E] (s : set E) :
Prop

A set s is von Neumann bounded if every neighborhood of 0 absorbs s.

Equations
@[simp]
theorem bornology.is_vonN_bounded_empty (𝕜 : Type u_1) (E : Type u_3) [ E] [has_zero E]  :
theorem bornology.is_vonN_bounded_iff {𝕜 : Type u_1} {E : Type u_3} [ E] [has_zero E] (s : set E) :
(V : set E), V nhds 0 V s
theorem filter.has_basis.is_vonN_bounded_basis_iff {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_6} [ E] [has_zero E] {q : ι Prop} {s : ι set E} {A : set E} (h : (nhds 0).has_basis q s) :
(i : ι), q i (s i) A
theorem bornology.is_vonN_bounded.subset {𝕜 : Type u_1} {E : Type u_3} [ E] [has_zero E] {s₁ s₂ : set E} (h : s₁ s₂) (hs₂ : s₂) :

Subsets of bounded sets are bounded.

theorem bornology.is_vonN_bounded.union {𝕜 : Type u_1} {E : Type u_3} [ E] [has_zero E] {s₁ s₂ : set E} (hs₁ : s₁) (hs₂ : s₂) :
(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} [ E] {t t' : topological_space E} (h : t t') {s : set E} (hs : 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} [module 𝕜₁ E] [module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} {s : set E} (hs : s) (f : E →SL[σ] F) :
(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 𝕜] [ E] {S : set E} {ε : ι 𝕜} {x : ι E} {l : filter ι} (hS : S) (hxS : ∀ᶠ (n : ι) in l, x n S) (hε : (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} [ E] [ 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} [ E] [ E] {ε : ι 𝕝} {l : filter ι} [l.ne_bot] (hε : {0})) {S : set E} :
(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 𝕜] [ E] [ E] (x : E) :

Singletons are bounded.

theorem bornology.is_vonN_bounded_covers {𝕜 : Type u_1} {E : Type u_3} [normed_field 𝕜] [ E] [ 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 𝕜] [ E] [ 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 𝕜] [ E] [ E] {s : set E} :
theorem totally_bounded.is_vonN_bounded (𝕜 : Type u_1) {E : Type u_3} [ E] [ E] {s : set E} (hs : totally_bounded s) :
theorem normed_space.is_vonN_bounded_ball (𝕜 : Type u_1) (E : Type u_3) [ E] (r : ) :
theorem normed_space.is_vonN_bounded_closed_ball (𝕜 : Type u_1) (E : Type u_3) [ E] (r : ) :
theorem normed_space.is_vonN_bounded_iff (𝕜 : Type u_1) (E : Type u_3) [ E] (s : set E) :
theorem normed_space.is_vonN_bounded_iff' (𝕜 : Type u_1) (E : Type u_3) [ E] (s : set E) :
(r : ), (x : E), x s x r
theorem normed_space.image_is_vonN_bounded_iff (𝕜 : Type u_1) (E : Type u_3) {E' : Type u_4} [ E] (f : E' E) (s : set E') :
(f '' s) (r : ), (x : E'), x s f x r
theorem normed_space.vonN_bornology_eq (𝕜 : Type u_1) (E : Type u_3) [ 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) [ E] {s : set E} :
(a : 𝕜), s a 1
theorem normed_space.is_bounded_iff_subset_smul_closed_ball (𝕜 : Type u_1) (E : Type u_3) [ E] {s : set E} :
(a : 𝕜), s a