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.

Equations
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 Vnhds 0, Absorbs 𝕜 V s
    theorem Filter.HasBasis.isVonNBounded_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 : (nhds 0).HasBasis q s) :
    Bornology.IsVonNBounded 𝕜 A ∀ (i : ι), q iAbsorbs 𝕜 (s i) A
    @[deprecated Filter.HasBasis.isVonNBounded_iff]
    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 : (nhds 0).HasBasis q s) :
    Bornology.IsVonNBounded 𝕜 A ∀ (i : ι), q iAbsorbs 𝕜 (s i) A

    Alias of Filter.HasBasis.isVonNBounded_iff.

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

    Subsets of bounded sets are bounded.

    @[simp]
    theorem Bornology.isVonNBounded_union {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {s : Set E} {t : Set E} :
    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_boundedSpace {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] [BoundedSpace 𝕜] {s : Set E} :
    @[simp]
    theorem Bornology.isVonNBounded_iUnion {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {ι : Sort u_7} [Finite ι] {s : ιSet E} :
    Bornology.IsVonNBounded 𝕜 (⋃ (i : ι), s i) ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (s i)
    theorem Bornology.isVonNBounded_biUnion {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {ι : Type u_7} {I : Set ι} (hI : I.Finite) {s : ιSet E} :
    Bornology.IsVonNBounded 𝕜 (⋃ iI, s i) iI, Bornology.IsVonNBounded 𝕜 (s i)
    theorem Bornology.isVonNBounded_sUnion {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [SMul 𝕜 E] [Zero E] [TopologicalSpace E] {S : Set (Set E)} (hS : S.Finite) :
    theorem Bornology.IsVonNBounded.add {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddZeroClass E] [TopologicalSpace E] [ContinuousAdd E] [DistribSMul 𝕜 E] {s : Set E} {t : Set E} (hs : Bornology.IsVonNBounded 𝕜 s) (ht : Bornology.IsVonNBounded 𝕜 t) :

    Alias of the forward direction of Bornology.isVonNBounded_neg.

    theorem Bornology.IsVonNBounded.sub {𝕜 : Type u_1} {E : Type u_3} [SeminormedRing 𝕜] [AddGroup E] [TopologicalSpace E] [TopologicalAddGroup E] [DistribMulAction 𝕜 E] {s : Set E} {t : Set E} (hs : Bornology.IsVonNBounded 𝕜 s) (ht : Bornology.IsVonNBounded 𝕜 t) :
    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_iff_tendsto_smallSets_nhds {𝕜 : Type u_7} {E : Type u_8} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
    Bornology.IsVonNBounded 𝕜 S Filter.Tendsto (fun (x : 𝕜) => x S) (nhds 0) (nhds 0).smallSets
    theorem Bornology.IsVonNBounded.tendsto_smallSets_nhds {𝕜 : Type u_7} {E : Type u_8} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
    Bornology.IsVonNBounded 𝕜 SFilter.Tendsto (fun (x : 𝕜) => x S) (nhds 0) (nhds 0).smallSets

    Alias of the forward direction of Bornology.isVonNBounded_iff_tendsto_smallSets_nhds.

    theorem Bornology.isVonNBounded_pi_iff {𝕜 : Type u_7} {ι : Type u_8} {E : ιType u_9} [NormedDivisionRing 𝕜] [(i : ι) → AddCommGroup (E i)] [(i : ι) → Module 𝕜 (E i)] [(i : ι) → TopologicalSpace (E i)] {S : Set ((i : ι) → E i)} :
    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 {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι𝕜} {l : Filter ι} [l.NeBot] (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 {𝕜 : Type u_1} {E : Type u_3} {ι : Type u_6} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] {ε : ι𝕜} {l : Filter ι} [l.NeBot] (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.extend_scalars {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_7} [AddCommGroup E] [Module 𝕜 E] (𝕝 : Type u_8) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {s : Set E} (h : Bornology.IsVonNBounded 𝕜 s) :

    If a set is von Neumann bounded with respect to a smaller field, then it is also von Neumann bounded with respect to a larger field. See also Bornology.IsVonNBounded.restrict_scalars below.

    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.

    @[simp]
    theorem Bornology.isVonNBounded_insert {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) {s : Set E} :
    theorem Bornology.IsVonNBounded.insert {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] (x : E) {s : Set E} :

    Alias of the reverse direction of Bornology.isVonNBounded_insert.

    theorem Bornology.IsVonNBounded.vadd {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} (hs : Bornology.IsVonNBounded 𝕜 s) (x : E) :
    @[simp]
    theorem Bornology.isVonNBounded_vadd {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} (x : E) :
    theorem Bornology.IsVonNBounded.of_add_right {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} {t : Set E} (hst : Bornology.IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) :
    theorem Bornology.IsVonNBounded.of_add_left {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} {t : Set E} (hst : Bornology.IsVonNBounded 𝕜 (s + t)) (ht : t.Nonempty) :
    theorem Bornology.isVonNBounded_add_of_nonempty {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} {t : Set E} (hs : s.Nonempty) (ht : t.Nonempty) :
    @[simp]
    theorem Bornology.IsVonNBounded.of_sub_left {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [ContinuousAdd E] {s : Set E} {t : Set E} (hst : Bornology.IsVonNBounded 𝕜 (s - t)) (ht : t.Nonempty) :
    theorem Bornology.IsVonNBounded.of_sub_right {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [TopologicalAddGroup E] {s : Set E} {t : Set E} (hst : Bornology.IsVonNBounded 𝕜 (s - t)) (hs : s.Nonempty) :
    theorem Bornology.isVonNBounded_sub_of_nonempty {𝕜 : Type u_1} {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [ContinuousSMul 𝕜 E] [TopologicalAddGroup E] {s : Set E} {t : Set E} (hs : s.Nonempty) (ht : t.Nonempty) :
    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, inline]
    abbrev 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.

    Equations
    Instances For
      theorem TotallyBounded.isVonNBounded (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [UniformSpace E] [UniformAddGroup E] [ContinuousSMul 𝕜 E] {s : Set E} (hs : TotallyBounded s) :
      theorem Filter.Tendsto.isVonNBounded_range (𝕜 : Type u_1) {E : Type u_3} [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul 𝕜 E] {f : E} {x : E} (hf : Filter.Tendsto f Filter.atTop (nhds x)) :
      theorem Bornology.IsVonNBounded.restrict_scalars_of_nontrivial (𝕜 : Type u_1) {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] [Zero E] [TopologicalSpace E] [SMul 𝕜 E] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E} (h : Bornology.IsVonNBounded 𝕜' s) :
      theorem Bornology.IsVonNBounded.restrict_scalars (𝕜 : Type u_1) {𝕜' : Type u_2} {E : Type u_3} [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Zero E] [TopologicalSpace E] [SMul 𝕜 E] [MulActionWithZero 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E} (h : Bornology.IsVonNBounded 𝕜' s) :
      theorem NormedSpace.isVonNBounded_iff' (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} :
      Bornology.IsVonNBounded 𝕜 s ∃ (r : ), xs, x r
      theorem NormedSpace.image_isVonNBounded_iff (𝕜 : Type u_1) {E : Type u_3} [NontriviallyNormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {α : Type u_7} {f : αE} {s : Set α} :
      Bornology.IsVonNBounded 𝕜 (f '' s) ∃ (r : ), xs, 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.