Von Neumann Boundedness

This file defines natural or von Neumann bounded sets and proves elementary properties.

Main declarations

• Bornology.IsVonNBounded: A set s is von Neumann-bounded if every neighborhood of zero absorbs s.
• Bornology.vonNBornology: The bornology made of the von Neumann-bounded sets.

Main results

• Bornology.IsVonNBounded.of_topologicalSpace_le: A coarser topology admits more von Neumann-bounded sets.
• Bornology.IsVonNBounded.image: A continuous linear image of a bounded set is bounded.
• Bornology.isVonNBounded_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

• [Bourbaki, Topological Vector Spaces][bourbaki1987]

def Bornology.IsVonNBounded (𝕜 : Type u_1) {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] (s : Set E) : Prop

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

Equations

• Bornology.IsVonNBounded 𝕜 s = ∀ ⦃V : Set E⦄, V ∈ nhds 0 → Absorbs 𝕜 V s

@[simp]

theorem Bornology.isVonNBounded_empty (𝕜 : Type u_1) (E : Type u_3) [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] : Bornology.IsVonNBounded 𝕜 ∅

theorem Bornology.isVonNBounded_iff {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] (s : Set E) : Bornology.IsVonNBounded 𝕜 s ↔ ∀ (V : Set E), V ∈ nhds 0 → Absorbs 𝕜 V s

theorem Filter.HasBasis.isVonNBounded_basis_iff {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_6} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {q : ι → Prop} {s : ι → Set E} {A : Set E} (h : Filter.HasBasis (nhds 0) q s) : Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (s i) A

theorem Bornology.IsVonNBounded.subset {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {s₁ : Set E} {s₂ : Set E} (h : s₁ ⊆ s₂) (hs₂ : Bornology.IsVonNBounded 𝕜 s₂) : Bornology.IsVonNBounded 𝕜 s₁

Subsets of bounded sets are bounded.

theorem Bornology.IsVonNBounded.union {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {s₁ : Set E} {s₂ : Set E} (hs₁ : Bornology.IsVonNBounded 𝕜 s₁) (hs₂ : Bornology.IsVonNBounded 𝕜 s₂) : Bornology.IsVonNBounded 𝕜 (s₁ ∪ s₂)

The union of two bounded sets is bounded.

theorem Bornology.IsVonNBounded.of_topologicalSpace_le {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {t : TopologicalSpace E} {t' : TopologicalSpace E} (h : t ≤ t') {s : Set E} (hs : Bornology.IsVonNBounded 𝕜 s) : Bornology.IsVonNBounded 𝕜 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.IsVonNBounded.image {E : Type u_3} {F : Type u_5} {𝕜₁ : Type u_7} {𝕜₂ : Type u_8} [NormedDivisionRing 𝕜₁] [NormedDivisionRing 𝕜₂] [AddCommGroup E] [Module 𝕜₁ E] [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace E] [TopologicalSpace F] {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ] [RingHomIsometric σ] {s : Set E} (hs : Bornology.IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) : Bornology.IsVonNBounded 𝕜₂ (↑f '' s)

A continuous linear image of a bounded set is bounded.

theorem Bornology.IsVonNBounded.smul_tendsto_zero {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_6} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} {ε : ι → 𝕜} {x : ι → E} {l : Filter ι} (hS : Bornology.IsVonNBounded 𝕜 S) (hxS : ∀ᶠ (n : ι) in l, x n ∈ S) (hε : Filter.Tendsto ε l (nhds 0)) : Filter.Tendsto (ε • x) l (nhds 0)

theorem Bornology.isVonNBounded_of_smul_tendsto_zero {E : Type u_3} {ι : Type u_6} {𝕝 : Type u_7} [NontriviallyNormedField 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] {ε : ι → 𝕝} {l : Filter ι} [Filter.NeBot l] (hε : ∀ᶠ (n : ι) in l, ε n ≠ 0) {S : Set E} (H : ∀ (x : ι → E), (∀ (n : ι), x n ∈ S) → Filter.Tendsto (ε • x) l (nhds 0)) : Bornology.IsVonNBounded 𝕝 S

theorem Bornology.isVonNBounded_iff_smul_tendsto_zero {E : Type u_3} {ι : Type u_6} {𝕝 : Type u_7} [NontriviallyNormedField 𝕝] [AddCommGroup E] [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] {ε : ι → 𝕝} {l : Filter ι} [Filter.NeBot l] (hε : Filter.Tendsto ε l (nhdsWithin 0 {0}ᶜ)) {S : Set E} : Bornology.IsVonNBounded 𝕝 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.isVonNBounded_singleton {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) : Bornology.IsVonNBounded 𝕜 {x}

Singletons are bounded.

theorem Bornology.isVonNBounded_covers {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] : ⋃₀ setOf (Bornology.IsVonNBounded 𝕜) = Set.univ

The union of all bounded set is the whole space.

@[reducible]

def Bornology.vonNBornology (𝕜 : Type u_1) (E : Type u_3) [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] : Bornology 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

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bornology.isBounded_iff_isVonNBounded (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {s : Set E} : Bornology.IsBounded s ↔ Bornology.IsVonNBounded 𝕜 s

theorem TotallyBounded.isVonNBounded (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : TotallyBounded s) : Bornology.IsVonNBounded 𝕜 s

theorem NormedSpace.isVonNBounded_ball (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : ℝ) : Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)

theorem NormedSpace.isVonNBounded_closedBall (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (r : ℝ) : Bornology.IsVonNBounded 𝕜 (Metric.closedBall 0 r)

theorem NormedSpace.isVonNBounded_iff (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

theorem NormedSpace.isVonNBounded_iff' (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (s : Set E) : Bornology.IsVonNBounded 𝕜 s ↔ ∃ r, ∀ (x : E), x ∈ s → ‖x‖ ≤ r

theorem NormedSpace.image_isVonNBounded_iff (𝕜 : Type u_1) (E : Type u_3) {E' : Type u_4} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (f : E' → E) (s : Set E') : Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r, ∀ (x : E'), x ∈ s → ‖f x‖ ≤ r

theorem NormedSpace.vonNBornology_eq (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology

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

theorem NormedSpace.isBounded_iff_subset_smul_ball (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.ball 0 1

theorem NormedSpace.isBounded_iff_subset_smul_closedBall (𝕜 : Type u_1) (E : Type u_3) [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : Bornology.IsBounded s ↔ ∃ a, s ⊆ a • Metric.closedBall 0 1