Documentation

Mathlib.Analysis.LocallyConvex.Bounded

Von Neumann Boundedness #

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

Main declarations #

Main results #

References #

def Bornology.IsVonNBounded (๐•œ : Type u_1) {E : Type u_3} [SeminormedRing ๐•œ] [SMul ๐•œ E] [Zero E] [TopologicalSpace E] (s : Set E) :

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

Instances For
    @[simp]
    theorem Bornology.isVonNBounded_empty (๐•œ : Type u_1) (E : Type u_3) [SeminormedRing ๐•œ] [SMul ๐•œ E] [Zero E] [TopologicalSpace E] :
    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) :

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

    Singletons are bounded.

    theorem Bornology.isVonNBounded_covers {๐•œ : Type u_1} {E : Type u_3} [NormedField ๐•œ] [AddCommGroup E] [Module ๐•œ E] [TopologicalSpace E] [ContinuousSMul ๐•œ E] :

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

    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.

    Instances For
      @[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} :
      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) :
      theorem NormedSpace.isVonNBounded_ball (๐•œ : Type u_1) (E : Type u_3) [NontriviallyNormedField ๐•œ] [SeminormedAddCommGroup E] [NormedSpace ๐•œ E] (r : โ„) :
      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.