mathlib documentation

analysis.locally_convex.bounded

Von Neumann Boundedness #

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_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) :
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β‚‚) :
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_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.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') :

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