mathlib3 documentation

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 #

Main results #

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.

Equations
@[simp]
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) :
bornology.is_vonN_bounded 𝕜 s (V : set E), V nhds 0 absorbs 𝕜 V s
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₂) :

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) :

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.

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
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') :
bornology.is_vonN_bounded 𝕜 (f '' s) (r : ), (x : E'), x s f x r

In a normed space, the von Neumann bornology (bornology.vonN_bornology) is equal to the metric bornology.