Mathlib.Analysis.LocallyConvex.Bounded

Bornology.IsVonNBounded definition

(s : Set E) : Prop

Full source

/-- A set `s` is von Neumann bounded if every neighborhood of 0 absorbs `s`. -/
def IsVonNBounded (s : Set E) : Prop :=
  ∀ ⦃V⦄, V ∈ 𝓝 (0 : E) → Absorbs 𝕜 V s

Von Neumann bounded set

Informal description

A subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$ is called *von Neumann bounded* if for every neighborhood $V$ of zero in $E$, $V$ absorbs $s$ (i.e., there exists a scalar $\lambda$ such that $s \subseteq \lambda V$).

Bornology.isVonNBounded_empty theorem

: IsVonNBounded 𝕜 (∅ : Set E)

Full source

@[simp]
theorem isVonNBounded_empty : IsVonNBounded 𝕜 (∅ : Set E) := fun _ _ => Absorbs.empty

Empty Set is Von Neumann Bounded

Informal description

The empty set is von Neumann bounded in any topological vector space $E$ over a field $\mathbb{K}$.

Bornology.isVonNBounded_iff theorem

(s : Set E) : IsVonNBounded 𝕜 s ↔ ∀ V ∈ 𝓝 (0 : E), Absorbs 𝕜 V s

Full source

theorem isVonNBounded_iff (s : Set E) : IsVonNBoundedIsVonNBounded 𝕜 s ↔ ∀ V ∈ 𝓝 (0 : E), Absorbs 𝕜 V s :=
  Iff.rfl

Characterization of Von Neumann Bounded Sets via Neighborhood Absorption

Informal description

A subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$ is von Neumann bounded if and only if for every neighborhood $V$ of zero in $E$, there exists a scalar $\lambda \in \mathbb{K}$ such that $s \subseteq \lambda V$.

Filter.HasBasis.isVonNBounded_iff theorem

 {q : ι → Prop} {s : ι → Set E} {A : Set E} (h : (𝓝 (0 : E)).HasBasis q s) :
  IsVonNBounded 𝕜 A ↔ ∀ i, q i → Absorbs 𝕜 (s i) A

Full source

theorem _root_.Filter.HasBasis.isVonNBounded_iff {q : ι → Prop} {s : ι → Set E} {A : Set E}
    (h : (𝓝 (0 : E)).HasBasis q s) : IsVonNBoundedIsVonNBounded 𝕜 A ↔ ∀ i, q i → Absorbs 𝕜 (s i) A := by
  refine ⟨fun hA i hi => hA (h.mem_of_mem hi), fun hA V hV => ?_⟩
  rcases h.mem_iff.mp hV with ⟨i, hi, hV⟩
  exact (hA i hi).mono_left hV

Characterization of Von Neumann Bounded Sets via Filter Basis

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$, and let $\mathcal{N}(0)$ be the neighborhood filter of zero in $E$. Suppose $\mathcal{N}(0)$ has a basis $\{s_i\}_{i \in \iota}$ indexed by a predicate $q$ (i.e., $V \in \mathcal{N}(0)$ if and only if there exists $i$ such that $q(i)$ holds and $s_i \subseteq V$). Then, a subset $A \subseteq E$ is von Neumann bounded if and only if for every index $i$ satisfying $q(i)$, the set $s_i$ absorbs $A$.

Bornology.IsVonNBounded.subset theorem

{s₁ s₂ : Set E} (h : s₁ ⊆ s₂) (hs₂ : IsVonNBounded 𝕜 s₂) : IsVonNBounded 𝕜 s₁

Full source

/-- Subsets of bounded sets are bounded. -/
theorem IsVonNBounded.subset {s₁ s₂ : Set E} (h : s₁ ⊆ s₂) (hs₂ : IsVonNBounded 𝕜 s₂) :
    IsVonNBounded 𝕜 s₁ := fun _ hV => (hs₂ hV).mono_right h

Subsets of von Neumann bounded sets are bounded

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If $s_1$ is a subset of $s_2$ and $s_2$ is von Neumann bounded, then $s_1$ is also von Neumann bounded.

Bornology.isVonNBounded_union theorem

{s t : Set E} : IsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Full source

@[simp]
theorem isVonNBounded_union {s t : Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 (s ∪ t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t := by
  simp only [IsVonNBounded, absorbs_union, forall_and]

Union of Von Neumann Bounded Sets is Bounded if and only if Each Set is Bounded

Informal description

For any two subsets $s$ and $t$ of a topological vector space $E$ over a field $\mathbb{K}$, the union $s \cup t$ is von Neumann bounded if and only if both $s$ and $t$ are von Neumann bounded individually.

Bornology.IsVonNBounded.union theorem

 {s₁ s₂ : Set E} (hs₁ : IsVonNBounded 𝕜 s₁) (hs₂ : IsVonNBounded 𝕜 s₂) : IsVonNBounded 𝕜 (s₁ ∪ s₂)

Full source

/-- The union of two bounded sets is bounded. -/
theorem IsVonNBounded.union {s₁ s₂ : Set E} (hs₁ : IsVonNBounded 𝕜 s₁) (hs₂ : IsVonNBounded 𝕜 s₂) :
    IsVonNBounded 𝕜 (s₁ ∪ s₂) := isVonNBounded_union.2 ⟨hs₁, hs₂⟩

Union of von Neumann Bounded Sets is Bounded

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If $s_1$ and $s_2$ are von Neumann bounded subsets of $E$, then their union $s_1 \cup s_2$ is also von Neumann bounded.

Bornology.IsVonNBounded.of_boundedSpace theorem

[BoundedSpace 𝕜] {s : Set E} : IsVonNBounded 𝕜 s

Full source

@[nontriviality]
theorem IsVonNBounded.of_boundedSpace [BoundedSpace 𝕜] {s : Set E} : IsVonNBounded 𝕜 s := fun _ _ ↦
  .of_boundedSpace

All subsets are von Neumann bounded in a bounded topological vector space

Informal description

In a topological vector space $E$ over a field $\mathbb{K}$ that is a bounded space (i.e., the entire space $E$ is von Neumann bounded), every subset $s \subseteq E$ is von Neumann bounded.

Bornology.IsVonNBounded.of_subsingleton theorem

[Subsingleton E] {s : Set E} : IsVonNBounded 𝕜 s

Full source

@[nontriviality]
theorem IsVonNBounded.of_subsingleton [Subsingleton E] {s : Set E} : IsVonNBounded 𝕜 s :=
  fun U hU ↦ .of_forall fun c ↦ calc
    s ⊆ univ := subset_univ s
    _ = c • U := .symm <| Subsingleton.eq_univ_of_nonempty <| (Filter.nonempty_of_mem hU).image _

Von Neumann Boundedness of Subsets in a Subsingleton Space

Informal description

For any subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$, if $E$ is a subsingleton (i.e., has at most one element), then $s$ is von Neumann bounded.

Bornology.isVonNBounded_iUnion theorem

{ι : Sort*} [Finite ι] {s : ι → Set E} : IsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ i, IsVonNBounded 𝕜 (s i)

Full source

@[simp]
theorem isVonNBounded_iUnion {ι : Sort*} [Finite ι] {s : ι → Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 (⋃ i, s i) ↔ ∀ i, IsVonNBounded 𝕜 (s i) := by
  simp only [IsVonNBounded, absorbs_iUnion, @forall_swap ι]

Finite Union of Von Neumann Bounded Sets is Von Neumann Bounded if and only if Each Set is Bounded

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$, and let $\{s_i\}_{i \in \iota}$ be a finite family of subsets of $E$. Then the union $\bigcup_{i \in \iota} s_i$ is von Neumann bounded if and only if each $s_i$ is von Neumann bounded.

Bornology.isVonNBounded_biUnion theorem

 {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set E} :
  IsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i)

Full source

theorem isVonNBounded_biUnion {ι : Type*} {I : Set ι} (hI : I.Finite) {s : ι → Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 (⋃ i ∈ I, s i) ↔ ∀ i ∈ I, IsVonNBounded 𝕜 (s i) := by
  have _ := hI.to_subtype
  rw [biUnion_eq_iUnion, isVonNBounded_iUnion, Subtype.forall]

Finite Indexed Union is Von Neumann Bounded if and only if Each Member is Bounded

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$, and let $\{s_i\}_{i \in \iota}$ be a family of subsets of $E$ indexed by a finite set $I \subseteq \iota$. Then the union $\bigcup_{i \in I} s_i$ is von Neumann bounded if and only if for each $i \in I$, the subset $s_i$ is von Neumann bounded.

Bornology.isVonNBounded_sUnion theorem

{S : Set (Set E)} (hS : S.Finite) : IsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s

Full source

theorem isVonNBounded_sUnion {S : Set (Set E)} (hS : S.Finite) :
    IsVonNBoundedIsVonNBounded 𝕜 (⋃₀ S) ↔ ∀ s ∈ S, IsVonNBounded 𝕜 s := by
  rw [sUnion_eq_biUnion, isVonNBounded_biUnion hS]

Finite Union is Von Neumann Bounded if and only if All Members are Bounded

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$, and let $S$ be a finite collection of subsets of $E$. The union $\bigcup S$ is von Neumann bounded if and only if every set $s \in S$ is von Neumann bounded.

Bornology.IsVonNBounded.add theorem

(hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) : IsVonNBounded 𝕜 (s + t)

Full source

protected theorem IsVonNBounded.add (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) :
    IsVonNBounded 𝕜 (s + t) := fun U hU ↦ by
  rcases exists_open_nhds_zero_add_subset hU with ⟨V, hVo, hV, hVU⟩
  exact ((hs <| hVo.mem_nhds hV).add (ht <| hVo.mem_nhds hV)).mono_left hVU

Von Neumann Boundedness is Preserved under Minkowski Sum

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If two subsets $s$ and $t$ of $E$ are von Neumann bounded, then their Minkowski sum $s + t = \{x + y \mid x \in s, y \in t\}$ is also von Neumann bounded.

Bornology.IsVonNBounded.neg theorem

(hs : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕜 (-s)

Full source

protected theorem IsVonNBounded.neg (hs : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕜 (-s) := fun U hU ↦ by
  rw [← neg_neg U]
  exact (hs <| neg_mem_nhds_zero _ hU).neg_neg

Negation Preserves Von Neumann Boundedness

Informal description

If a subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$ is von Neumann bounded, then its negation $-s$ is also von Neumann bounded.

Bornology.isVonNBounded_neg theorem

: IsVonNBounded 𝕜 (-s) ↔ IsVonNBounded 𝕜 s

Full source

@[simp]
theorem isVonNBounded_neg : IsVonNBoundedIsVonNBounded 𝕜 (-s) ↔ IsVonNBounded 𝕜 s :=
  ⟨fun h ↦ neg_neg s ▸ h.neg, fun h ↦ h.neg⟩

Von Neumann Boundedness is Equivalent for a Set and its Negation

Informal description

A subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$ is von Neumann bounded if and only if its negation $-s$ is von Neumann bounded.

Bornology.IsVonNBounded.sub theorem

(hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) : IsVonNBounded 𝕜 (s - t)

Full source

protected theorem IsVonNBounded.sub (hs : IsVonNBounded 𝕜 s) (ht : IsVonNBounded 𝕜 t) :
    IsVonNBounded 𝕜 (s - t) := by
  rw [sub_eq_add_neg]
  exact hs.add ht.neg

Von Neumann Boundedness is Preserved under Set Difference

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If two subsets $s$ and $t$ of $E$ are von Neumann bounded, then their set difference $s - t = \{x - y \mid x \in s, y \in t\}$ is also von Neumann bounded.

Bornology.IsVonNBounded.of_topologicalSpace_le theorem

 {t t' : TopologicalSpace E} (h : t ≤ t') {s : Set E} (hs : @IsVonNBounded 𝕜 E _ _ _ t s) :
  @IsVonNBounded 𝕜 E _ _ _ t' s

Full source

/-- 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 IsVonNBounded.of_topologicalSpace_le {t t' : TopologicalSpace E} (h : t ≤ t') {s : Set E}
    (hs : @IsVonNBounded 𝕜 E _ _ _ t s) : @IsVonNBounded 𝕜 E _ _ _ t' s := fun _ hV =>
  hs <| (le_iff_nhds t t').mp h 0 hV

Von Neumann Boundedness under Coarser Topology

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$ with two topologies $t$ and $t'$ such that $t'$ is coarser than $t$ (i.e., $t \leq t'$). If a subset $s \subseteq E$ is von Neumann bounded with respect to $t$, then $s$ is also von Neumann bounded with respect to $t'$.

Bornology.isVonNBounded_iff_tendsto_smallSets_nhds theorem

 {𝕜 E : Type*} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
  IsVonNBounded 𝕜 S ↔ Tendsto (· • S : 𝕜 → Set E) (𝓝 0) (𝓝 0).smallSets

Full source

lemma isVonNBounded_iff_tendsto_smallSets_nhds {𝕜 E : Type*} [NormedDivisionRing 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 S ↔ Tendsto (· • S : 𝕜 → Set E) (𝓝 0) (𝓝 0).smallSets := by
  rw [tendsto_smallSets_iff]
  refine forall₂_congr fun V hV ↦ ?_
  simp only [absorbs_iff_eventually_nhds_zero (mem_of_mem_nhds hV), mapsTo', image_smul]

Von Neumann Boundedness Criterion via Scalar Multiplication Tendency to Zero

Informal description

Let $\mathbb{K}$ be a normed division ring and $E$ be a topological vector space over $\mathbb{K}$. A subset $S \subseteq E$ is von Neumann bounded if and only if the scalar multiplication map $\lambda \mapsto \lambda \cdot S$ tends to the zero neighborhood filter $\mathcal{N}_0$ in the small sets filter of $\mathcal{N}_0$ as $\lambda$ tends to $0$ in $\mathbb{K}$.

Bornology.isVonNBounded_iff_absorbing_le theorem

 {𝕜 E : Type*} [NormedDivisionRing 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
  IsVonNBounded 𝕜 S ↔ Filter.absorbing 𝕜 S ≤ 𝓝 0

Full source

lemma isVonNBounded_iff_absorbing_le {𝕜 E : Type*} [NormedDivisionRing 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 S ↔ Filter.absorbing 𝕜 S ≤ 𝓝 0 :=
  .rfl

Von Neumann Boundedness Criterion via Absorbing Sets

Informal description

Let $E$ be a topological vector space over a normed division ring $\mathbb{K}$. A subset $S \subseteq E$ is von Neumann bounded if and only if the filter of absorbing sets of $S$ is contained in the neighborhood filter of zero in $E$.

Bornology.isVonNBounded_pi_iff theorem

 {𝕜 ι : Type*} {E : ι → Type*} [NormedDivisionRing 𝕜] [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
  [∀ i, TopologicalSpace (E i)] {S : Set (∀ i, E i)} : IsVonNBounded 𝕜 S ↔ ∀ i, IsVonNBounded 𝕜 (eval i '' S)

Full source

lemma isVonNBounded_pi_iff {𝕜 ι : Type*} {E : ι → Type*} [NormedDivisionRing 𝕜]
    [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)] [∀ i, TopologicalSpace (E i)]
    {S : Set (∀ i, E i)} : IsVonNBoundedIsVonNBounded 𝕜 S ↔ ∀ i, IsVonNBounded 𝕜 (eval i '' S) := by
  simp_rw [isVonNBounded_iff_tendsto_smallSets_nhds, nhds_pi, Filter.pi, smallSets_iInf,
    smallSets_comap_eq_comap_image, tendsto_iInf, tendsto_comap_iff, Function.comp_def,
    ← image_smul, image_image, eval, Pi.smul_apply, Pi.zero_apply]

Von Neumann Boundedness Criterion for Product Spaces

Informal description

Let $\mathbb{K}$ be a normed division ring, and for each $i$ in some index set $\iota$, let $E_i$ be an additive commutative group equipped with a $\mathbb{K}$-module structure and a topological space structure. A subset $S$ of the product space $\prod_{i \in \iota} E_i$ is von Neumann bounded in $\mathbb{K}$ if and only if for every index $i$, the projection of $S$ onto the $i$-th component $E_i$ is von Neumann bounded in $\mathbb{K}$.

Bornology.IsVonNBounded.image theorem

 {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ] [RingHomIsometric σ] {s : Set E} (hs : IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) :
  IsVonNBounded 𝕜₂ (f '' s)

Full source

/-- A continuous linear image of a bounded set is bounded. -/
protected theorem IsVonNBounded.image {σ : 𝕜₁ →+* 𝕜₂} [RingHomSurjective σ] [RingHomIsometric σ]
    {s : Set E} (hs : IsVonNBounded 𝕜₁ s) (f : E →SL[σ] F) : IsVonNBounded 𝕜₂ (f '' s) := by
  have σ_iso : Isometry σ := AddMonoidHomClass.isometry_of_norm σ fun x => RingHomIsometric.is_iso
  have : map σ (𝓝 0) = 𝓝 0 := by
    rw [σ_iso.isEmbedding.map_nhds_eq, σ.surjective.range_eq, nhdsWithin_univ, map_zero]
  have hf₀ : Tendsto f (𝓝 0) (𝓝 0) := f.continuous.tendsto' 0 0 (map_zero f)
  simp only [isVonNBounded_iff_tendsto_smallSets_nhds, ← this, tendsto_map'_iff] at hs ⊢
  simpa only [comp_def, image_smul_setₛₗ] using hf₀.image_smallSets.comp hs

Continuous Linear Image of a Von Neumann Bounded Set is Bounded

Informal description

Let $\mathbb{K}_1$ and $\mathbb{K}_2$ be normed fields, and let $E$ and $F$ be topological vector spaces over $\mathbb{K}_1$ and $\mathbb{K}_2$ respectively. Let $\sigma \colon \mathbb{K}_1 \to \mathbb{K}_2$ be a ring homomorphism that is surjective and isometric. If $s \subseteq E$ is a von Neumann bounded subset and $f \colon E \to F$ is a continuous linear map with respect to $\sigma$, then the image $f(s) \subseteq F$ is von Neumann bounded.

Bornology.IsVonNBounded.smul_tendsto_zero theorem

 [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] {S : Set E} {ε : ι → 𝕜} {x : ι → E} {l : Filter ι}
  (hS : IsVonNBounded 𝕜 S) (hxS : ∀ᶠ n in l, x n ∈ S) (hε : Tendsto ε l (𝓝 0)) : Tendsto (ε • x) l (𝓝 0)

Full source

theorem IsVonNBounded.smul_tendsto_zero [NormedField 𝕜]
    [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
    {S : Set E} {ε : ι → 𝕜} {x : ι → E} {l : Filter ι}
    (hS : IsVonNBounded 𝕜 S) (hxS : ∀ᶠ n in l, x n ∈ S) (hε : Tendsto ε l (𝓝 0)) :
    Tendsto (ε • x) l (𝓝 0) :=
  (hS.tendsto_smallSets_nhds.comp hε).of_smallSets <| hxS.mono fun _ ↦ smul_mem_smul_set

Convergence of Scaled Sequences in Von Neumann Bounded Sets

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a topological vector space over $\mathbb{K}$, and $S \subseteq E$ a von Neumann bounded subset. Given a sequence of scalars $\{\varepsilon_n\}_{n \in \iota}$ in $\mathbb{K}$ converging to $0$ along a filter $l$ on $\iota$, and a sequence $\{x_n\}_{n \in \iota}$ in $E$ such that $x_n \in S$ frequently in $l$, then the sequence $\{\varepsilon_n x_n\}_{n \in \iota}$ converges to $0$ in $E$.

Bornology.isVonNBounded_of_smul_tendsto_zero theorem

 {ε : ι → 𝕜} {l : Filter ι} [l.NeBot] (hε : ∀ᶠ n in l, ε n ≠ 0) {S : Set E}
  (H : ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0)) : IsVonNBounded 𝕜 S

Full source

theorem isVonNBounded_of_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [l.NeBot]
    (hε : ∀ᶠ n in l, ε n ≠ 0) {S : Set E}
    (H : ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0)) : IsVonNBounded 𝕜 S := by
  rw [(nhds_basis_balanced 𝕜 E).isVonNBounded_iff]
  by_contra! H'
  rcases H' with ⟨V, ⟨hV, hVb⟩, hVS⟩
  have : ∀ᶠ n in l, ∃ x : S, ε n • (x : E) ∉ V := by
    filter_upwards [hε] with n hn
    rw [absorbs_iff_norm] at hVS
    push_neg at hVS
    rcases hVS ‖(ε n)⁻¹‖ with ⟨a, haε, haS⟩
    rcases Set.not_subset.mp haS with ⟨x, hxS, hx⟩
    refine ⟨⟨x, hxS⟩, fun hnx => ?_⟩
    rw [← Set.mem_inv_smul_set_iff₀ hn] at hnx
    exact hx (hVb.smul_mono haε hnx)
  rcases this.choice with ⟨x, hx⟩
  refine Filter.frequently_false l (Filter.Eventually.frequently ?_)
  filter_upwards [hx,
    (H (_ ∘ x) fun n => (x n).2).eventually (eventually_mem_set.mpr hV)] using fun n => id

Von Neumann Boundedness via Scalar Multiplication Convergence to Zero

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a topological vector space over $\mathbb{K}$, and $S \subseteq E$ a subset. Let $\{\varepsilon_n\}_{n \in \iota}$ be a sequence of scalars in $\mathbb{K}$ converging to $0$ along a nontrivial filter $l$ on $\iota$, with $\varepsilon_n \neq 0$ frequently in $l$. If for every sequence $\{x_n\}_{n \in \iota}$ in $S$, the sequence $\{\varepsilon_n x_n\}_{n \in \iota}$ converges to $0$ in $E$, then $S$ is von Neumann bounded in $E$.

Bornology.isVonNBounded_iff_smul_tendsto_zero theorem

 {ε : ι → 𝕜} {l : Filter ι} [l.NeBot] (hε : Tendsto ε l (𝓝[≠] 0)) {S : Set E} :
  IsVonNBounded 𝕜 S ↔ ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0)

Full source

/-- 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 isVonNBounded_iff_smul_tendsto_zero {ε : ι → 𝕜} {l : Filter ι} [l.NeBot]
    (hε : Tendsto ε l (𝓝[≠] 0)) {S : Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 S ↔ ∀ x : ι → E, (∀ n, x n ∈ S) → Tendsto (ε • x) l (𝓝 0) :=
  ⟨fun hS _ hxS => hS.smul_tendsto_zero (Eventually.of_forall hxS) (le_trans hε nhdsWithin_le_nhds),
    isVonNBounded_of_smul_tendsto_zero (by exact hε self_mem_nhdsWithin)⟩

Von Neumann Boundedness via Scalar Multiplication Convergence to Zero

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a topological vector space over $\mathbb{K}$, and $S \subseteq E$ a subset. Let $\{\varepsilon_n\}_{n \in \iota}$ be a sequence of scalars in $\mathbb{K}$ converging to $0$ but never equal to $0$ along a nontrivial filter $l$ on $\iota$. Then $S$ is von Neumann bounded if and only if for every sequence $\{x_n\}_{n \in \iota}$ in $S$, the sequence $\{\varepsilon_n x_n\}_{n \in \iota}$ converges to $0$ in $E$.

Bornology.IsVonNBounded.extend_scalars theorem

 [NontriviallyNormedField 𝕜] {E : Type*} [AddCommGroup E] [Module 𝕜 E] (𝕝 : Type*) [NontriviallyNormedField 𝕝]
  [NormedAlgebra 𝕜 𝕝] [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E] {s : Set E}
  (h : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕝 s

Full source

/-- 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 IsVonNBounded.extend_scalars [NontriviallyNormedField 𝕜]
    {E : Type*} [AddCommGroup E] [Module 𝕜 E]
    (𝕝 : Type*) [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝]
    [Module 𝕝 E] [TopologicalSpace E] [ContinuousSMul 𝕝 E] [IsScalarTower 𝕜 𝕝 E]
    {s : Set E} (h : IsVonNBounded 𝕜 s) : IsVonNBounded 𝕝 s := by
  obtain ⟨ε, hε, hε₀⟩ : ∃ ε : ℕ → 𝕜, Tendsto ε atTop (𝓝 0) ∧ ∀ᶠ n in atTop, ε n ≠ 0 := by
    simpa only [tendsto_nhdsWithin_iff] using exists_seq_tendsto (𝓝[≠] (0 : 𝕜))
  refine isVonNBounded_of_smul_tendsto_zero (ε := (ε · • 1)) (by simpa) fun x hx ↦ ?_
  have := h.smul_tendsto_zero (.of_forall hx) hε
  simpa only [Pi.smul_def', smul_one_smul]

Von Neumann Boundedness is Preserved Under Field Extension

Informal description

Let $\mathbb{K}$ and $\mathbb{L}$ be nontrivially normed fields with $\mathbb{K} \subseteq \mathbb{L}$ and a normed algebra structure from $\mathbb{K}$ to $\mathbb{L}$. Let $E$ be a topological vector space over $\mathbb{K}$ that is also a module over $\mathbb{L}$ with compatible scalar multiplication (i.e., $\mathbb{L}$ acts on $E$ extending the $\mathbb{K}$-action via $(\lambda \cdot_{\mathbb{K}} x) = (\iota(\lambda) \cdot_{\mathbb{L}} x)$ where $\iota : \mathbb{K} \to \mathbb{L}$ is the inclusion). If a subset $s \subseteq E$ is von Neumann bounded with respect to $\mathbb{K}$, then it is also von Neumann bounded with respect to $\mathbb{L}$.

Bornology.isVonNBounded_singleton theorem

(x : E) : IsVonNBounded 𝕜 ({ x } : Set E)

Full source

/-- Singletons are bounded. -/
theorem isVonNBounded_singleton (x : E) : IsVonNBounded 𝕜 ({x} : Set E) := fun _ hV =>
  (absorbent_nhds_zero hV).absorbs

Von Neumann Boundedness of Singleton Sets

Informal description

For any element $x$ in a topological vector space $E$ over a field $\mathbb{K}$, the singleton set $\{x\}$ is von Neumann bounded. That is, for every neighborhood $V$ of zero in $E$, there exists a scalar $\lambda \in \mathbb{K}$ such that $\{x\} \subseteq \lambda V$.

Bornology.isVonNBounded_insert theorem

(x : E) {s : Set E} : IsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s

Full source

@[simp]
theorem isVonNBounded_insert (x : E) {s : Set E} :
    IsVonNBoundedIsVonNBounded 𝕜 (insert x s) ↔ IsVonNBounded 𝕜 s := by
  simp only [← singleton_union, isVonNBounded_union, isVonNBounded_singleton, true_and]

Insertion Preserves Von Neumann Boundedness

Informal description

For any element $x$ in a topological vector space $E$ over a field $\mathbb{K}$ and any subset $s \subseteq E$, the set obtained by inserting $x$ into $s$ is von Neumann bounded if and only if $s$ itself is von Neumann bounded.

Bornology.IsVonNBounded.vadd theorem

(hs : IsVonNBounded 𝕜 s) (x : E) : IsVonNBounded 𝕜 (x +ᵥ s)

Full source

protected theorem IsVonNBounded.vadd (hs : IsVonNBounded 𝕜 s) (x : E) :
    IsVonNBounded 𝕜 (x +ᵥ s) := by
  rw [← singleton_vadd]
  -- TODO: dot notation timeouts in the next line
  exact IsVonNBounded.add (isVonNBounded_singleton x) hs

Translation Preserves Von Neumann Boundedness

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If a subset $s \subseteq E$ is von Neumann bounded, then for any $x \in E$, the set $x + s = \{x + y \mid y \in s\}$ is also von Neumann bounded.

Bornology.isVonNBounded_vadd theorem

(x : E) : IsVonNBounded 𝕜 (x +ᵥ s) ↔ IsVonNBounded 𝕜 s

Full source

@[simp]
theorem isVonNBounded_vadd (x : E) : IsVonNBoundedIsVonNBounded 𝕜 (x +ᵥ s) ↔ IsVonNBounded 𝕜 s :=
  ⟨fun h ↦ by simpa using h.vadd (-x), fun h ↦ h.vadd x⟩

Translation Invariance of Von Neumann Boundedness

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. For any element $x \in E$ and subset $s \subseteq E$, the translated set $x + s$ is von Neumann bounded if and only if $s$ is von Neumann bounded.

Bornology.IsVonNBounded.of_add_right theorem

(hst : IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) : IsVonNBounded 𝕜 t

Full source

theorem IsVonNBounded.of_add_right (hst : IsVonNBounded 𝕜 (s + t)) (hs : s.Nonempty) :
    IsVonNBounded 𝕜 t :=
  let ⟨x, hx⟩ := hs
  (isVonNBounded_vadd x).mp <| hst.subset <| image_subset_image2_right hx

Von Neumann Boundedness of Second Summand in Bounded Sum

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If the Minkowski sum $s + t$ of two subsets $s, t \subseteq E$ is von Neumann bounded and $s$ is nonempty, then $t$ is von Neumann bounded.

Bornology.IsVonNBounded.of_add_left theorem

(hst : IsVonNBounded 𝕜 (s + t)) (ht : t.Nonempty) : IsVonNBounded 𝕜 s

Full source

theorem IsVonNBounded.of_add_left (hst : IsVonNBounded 𝕜 (s + t)) (ht : t.Nonempty) :
    IsVonNBounded 𝕜 s :=
  ((add_comm s t).subst hst).of_add_right ht

Von Neumann Boundedness of First Summand in Bounded Sum

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If the Minkowski sum $s + t$ of two subsets $s, t \subseteq E$ is von Neumann bounded and $t$ is nonempty, then $s$ is von Neumann bounded.

Bornology.isVonNBounded_add_of_nonempty theorem

(hs : s.Nonempty) (ht : t.Nonempty) : IsVonNBounded 𝕜 (s + t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Full source

theorem isVonNBounded_add_of_nonempty (hs : s.Nonempty) (ht : t.Nonempty) :
    IsVonNBoundedIsVonNBounded 𝕜 (s + t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t :=
  ⟨fun h ↦ ⟨h.of_add_left ht, h.of_add_right hs⟩, and_imp.2 IsVonNBounded.add⟩

Von Neumann Boundedness of Minkowski Sum for Nonempty Sets

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$, and let $s, t \subseteq E$ be nonempty subsets. The Minkowski sum $s + t$ is von Neumann bounded if and only if both $s$ and $t$ are von Neumann bounded.

Bornology.isVonNBounded_add theorem

: IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Full source

theorem isVonNBounded_add :
    IsVonNBoundedIsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t := by
  rcases s.eq_empty_or_nonempty with rfl | hs; · simp
  rcases t.eq_empty_or_nonempty with rfl | ht; · simp
  simp [hs.ne_empty, ht.ne_empty, isVonNBounded_add_of_nonempty hs ht]

Von Neumann Boundedness of Minkowski Sum in Terms of Summands

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$, and let $s, t \subseteq E$ be subsets. The Minkowski sum $s + t$ is von Neumann bounded if and only if either $s$ is empty, $t$ is empty, or both $s$ and $t$ are von Neumann bounded.

Bornology.isVonNBounded_add_self theorem

: IsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s

Full source

@[simp]
theorem isVonNBounded_add_self : IsVonNBoundedIsVonNBounded 𝕜 (s + s) ↔ IsVonNBounded 𝕜 s := by
  rcases s.eq_empty_or_nonempty with rfl | hs <;> simp [isVonNBounded_add_of_nonempty, *]

Von Neumann Boundedness of Minkowski Sum with Itself

Informal description

For any subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$, the Minkowski sum $s + s$ is von Neumann bounded if and only if $s$ itself is von Neumann bounded.

Bornology.IsVonNBounded.of_sub_left theorem

(hst : IsVonNBounded 𝕜 (s - t)) (ht : t.Nonempty) : IsVonNBounded 𝕜 s

Full source

theorem IsVonNBounded.of_sub_left (hst : IsVonNBounded 𝕜 (s - t)) (ht : t.Nonempty) :
    IsVonNBounded 𝕜 s :=
  ((sub_eq_add_neg s t).subst hst).of_add_left ht.neg

Von Neumann Boundedness of First Set in Bounded Difference

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If the set difference $s - t$ is von Neumann bounded and $t$ is nonempty, then $s$ is von Neumann bounded.

Bornology.IsVonNBounded.of_sub_right theorem

(hst : IsVonNBounded 𝕜 (s - t)) (hs : s.Nonempty) : IsVonNBounded 𝕜 t

Full source

theorem IsVonNBounded.of_sub_right (hst : IsVonNBounded 𝕜 (s - t)) (hs : s.Nonempty) :
    IsVonNBounded 𝕜 t :=
  (((sub_eq_add_neg s t).subst hst).of_add_right hs).of_neg

Von Neumann Boundedness of Second Set in Bounded Difference

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If the set difference $s - t$ is von Neumann bounded and $s$ is nonempty, then $t$ is von Neumann bounded.

Bornology.isVonNBounded_sub_of_nonempty theorem

(hs : s.Nonempty) (ht : t.Nonempty) : IsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Full source

theorem isVonNBounded_sub_of_nonempty (hs : s.Nonempty) (ht : t.Nonempty) :
    IsVonNBoundedIsVonNBounded 𝕜 (s - t) ↔ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t := by
  simp [sub_eq_add_neg, isVonNBounded_add_of_nonempty, hs, ht]

Von Neumann Boundedness of Difference Set for Nonempty Sets

Informal description

Let $s$ and $t$ be nonempty subsets of a topological vector space $E$ over a field $\mathbb{K}$. Then the difference set $s - t$ is von Neumann bounded if and only if both $s$ and $t$ are von Neumann bounded.

Bornology.isVonNBounded_sub theorem

: IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t

Full source

theorem isVonNBounded_sub :
    IsVonNBoundedIsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ IsVonNBounded 𝕜 s ∧ IsVonNBounded 𝕜 t := by
  simp [sub_eq_add_neg, isVonNBounded_add]

Von Neumann Boundedness of Set Difference: $s - t$ is bounded iff $s$ or $t$ is empty or both are bounded

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. For any subsets $s, t \subseteq E$, the set difference $s - t$ is von Neumann bounded if and only if either $s$ is empty, $t$ is empty, or both $s$ and $t$ are von Neumann bounded.

Bornology.isVonNBounded_covers theorem

: ⋃₀ setOf (IsVonNBounded 𝕜) = (Set.univ : Set E)

Full source

/-- The union of all bounded set is the whole space. -/
theorem isVonNBounded_covers : ⋃₀ setOf (IsVonNBounded 𝕜) = (Set.univ : Set E) :=
  Set.eq_univ_iff_forall.mpr fun x =>
    Set.mem_sUnion.mpr ⟨{x}, isVonNBounded_singleton _, Set.mem_singleton _⟩

Union of Von Neumann Bounded Sets Covers the Space

Informal description

The union of all von Neumann bounded subsets of a topological vector space $E$ over a field $\mathbb{K}$ is equal to the entire space $E$.

Bornology.vonNBornology abbrev

: Bornology E

Full source

/-- 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. -/
abbrev vonNBornology : Bornology E :=
  Bornology.ofBounded (setOf (IsVonNBounded 𝕜)) (isVonNBounded_empty 𝕜 E)
    (fun _ hs _ ht => hs.subset ht) (fun _ hs _ => hs.union) isVonNBounded_singleton

Von Neumann Bornology on a Topological Vector Space

Informal description

The von Neumann bornology on a topological vector space $E$ over a field $\mathbb{K}$ is the bornology consisting of all von Neumann bounded subsets of $E$. A subset $s \subseteq E$ is von Neumann bounded if for every neighborhood $V$ of zero in $E$, there exists a scalar $\lambda \in \mathbb{K}$ such that $s \subseteq \lambda V$.

Bornology.isBounded_iff_isVonNBounded theorem

{s : Set E} : @IsBounded _ (vonNBornology 𝕜 E) s ↔ IsVonNBounded 𝕜 s

Full source

@[simp]
theorem isBounded_iff_isVonNBounded {s : Set E} :
    @IsBounded _ (vonNBornology 𝕜 E) s ↔ IsVonNBounded 𝕜 s :=
  isBounded_ofBounded_iff _

Equivalence of Boundedness in von Neumann Bornology and von Neumann Boundedness

Informal description

For any subset $s$ of a topological vector space $E$ over a field $\mathbb{K}$, $s$ is bounded in the von Neumann bornology if and only if $s$ is von Neumann bounded. That is, $s$ is bounded in the bornology generated by von Neumann bounded sets precisely when $s$ is von Neumann bounded.

TotallyBounded.isVonNBounded theorem

{s : Set E} (hs : TotallyBounded s) : Bornology.IsVonNBounded 𝕜 s

Full source

theorem TotallyBounded.isVonNBounded {s : Set E} (hs : TotallyBounded s) :
    Bornology.IsVonNBounded 𝕜 s := by
  if h : ∃ x : 𝕜, 1 < ‖x‖ then
    letI : NontriviallyNormedField 𝕜 := ⟨h⟩
    rw [totallyBounded_iff_subset_finite_iUnion_nhds_zero] at hs
    intro U hU
    have h : Filter.Tendsto (fun x : E × E => x.fst + x.snd) (𝓝 0) (𝓝 0) :=
      continuous_add.tendsto' _ _ (zero_add _)
    have h' := (nhds_basis_balanced 𝕜 E).prod (nhds_basis_balanced 𝕜 E)
    simp_rw [← nhds_prod_eq, id] at h'
    rcases h.basis_left h' U hU with ⟨x, hx, h''⟩
    rcases hs x.snd hx.2.1 with ⟨t, ht, hs⟩
    refine Absorbs.mono_right ?_ hs
    rw [ht.absorbs_biUnion]
    have hx_fstsnd : x.fst + x.snd ⊆ U := add_subset_iff.mpr fun z1 hz1 z2 hz2 ↦
      h'' <| mk_mem_prod hz1 hz2
    refine fun y _ => Absorbs.mono_left ?_ hx_fstsnd
    -- TODO: with dot notation, Lean timeouts on the next line. Why?
    exact Absorbent.vadd_absorbs (absorbent_nhds_zero hx.1.1) hx.2.2.absorbs_self
  else
    haveI : BoundedSpace 𝕜 := ⟨Metric.isBounded_iff.2 ⟨1, by simp_all [dist_eq_norm]⟩⟩
    exact Bornology.IsVonNBounded.of_boundedSpace

Totally bounded sets are von Neumann bounded in topological vector spaces

Informal description

Let $E$ be a topological vector space over a field $\mathbb{K}$. If a subset $s \subseteq E$ is totally bounded, then $s$ is von Neumann bounded.

Filter.Tendsto.isVonNBounded_range theorem

 [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  {f : ℕ → E} {x : E} (hf : Tendsto f atTop (𝓝 x)) : Bornology.IsVonNBounded 𝕜 (range f)

Full source

theorem Filter.Tendsto.isVonNBounded_range [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
    [TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
    {f : ℕ → E} {x : E} (hf : Tendsto f atTop (𝓝 x)) : Bornology.IsVonNBounded 𝕜 (range f) :=
  letI := IsTopologicalAddGroup.toUniformSpace E
  haveI := isUniformAddGroup_of_addCommGroup (G := E)
  hf.cauchySeq.totallyBounded_range.isVonNBounded 𝕜

Convergent sequences have von Neumann bounded range

Informal description

Let $\mathbb{K}$ be a normed field, $E$ a topological vector space over $\mathbb{K}$ with continuous scalar multiplication, and $f : \mathbb{N} \to E$ a sequence in $E$ that converges to some $x \in E$. Then the range of $f$ is von Neumann bounded in $E$.

Bornology.IsVonNBounded.restrict_scalars_of_nontrivial theorem

 [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜'] [Zero E] [TopologicalSpace E] [SMul 𝕜 E]
  [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E} (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s

Full source

protected theorem Bornology.IsVonNBounded.restrict_scalars_of_nontrivial
    [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Nontrivial 𝕜']
    [Zero E] [TopologicalSpace E]
    [SMul 𝕜 E] [MulAction 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E}
    (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s := by
  intro V hV
  refine (h hV).restrict_scalars <| AntilipschitzWith.tendsto_cobounded (K := ‖(1 : 𝕜')‖₊‖(1 : 𝕜')‖₊⁻¹) ?_
  refine AntilipschitzWith.of_le_mul_nndist fun x y ↦ ?_
  rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← sub_smul, nnnorm_smul, ← div_eq_inv_mul,
    mul_div_cancel_right₀ _ (nnnorm_ne_zero_iff.2 one_ne_zero)]

Von Neumann Boundedness under Scalar Restriction for Nontrivial Normed Algebras

Informal description

Let $\mathbb{K}$ be a normed field, $\mathbb{K}'$ a normed ring with a nontrivial normed algebra structure over $\mathbb{K}$, and $E$ a topological vector space over $\mathbb{K}'$ with a compatible scalar multiplication over $\mathbb{K}$. If a subset $s \subseteq E$ is von Neumann bounded with respect to $\mathbb{K}'$, then it is also von Neumann bounded with respect to $\mathbb{K}$.

Bornology.IsVonNBounded.restrict_scalars theorem

 [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜'] [Zero E] [TopologicalSpace E] [SMul 𝕜 E] [MulActionWithZero 𝕜' E]
  [IsScalarTower 𝕜 𝕜' E] {s : Set E} (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s

Full source

protected theorem Bornology.IsVonNBounded.restrict_scalars
    [NormedField 𝕜] [NormedRing 𝕜'] [NormedAlgebra 𝕜 𝕜']
    [Zero E] [TopologicalSpace E]
    [SMul 𝕜 E] [MulActionWithZero 𝕜' E] [IsScalarTower 𝕜 𝕜' E] {s : Set E}
    (h : IsVonNBounded 𝕜' s) : IsVonNBounded 𝕜 s :=
  match subsingleton_or_nontrivial 𝕜' with
  | .inl _ =>
    have : Subsingleton E := MulActionWithZero.subsingleton 𝕜' E
    IsVonNBounded.of_subsingleton
  | .inr _ =>
    h.restrict_scalars_of_nontrivial _

Von Neumann Boundedness under Scalar Restriction

Informal description

Let $\mathbb{K}$ be a normed field, $\mathbb{K}'$ a normed ring with a normed algebra structure over $\mathbb{K}$, and $E$ a topological vector space over $\mathbb{K}'$ with a compatible scalar multiplication over $\mathbb{K}$. If a subset $s \subseteq E$ is von Neumann bounded with respect to $\mathbb{K}'$, then it is also von Neumann bounded with respect to $\mathbb{K}$.

NormedSpace.isVonNBounded_of_isBounded theorem

{s : Set E} (h : Bornology.IsBounded s) : Bornology.IsVonNBounded 𝕜 s

Full source

theorem isVonNBounded_of_isBounded {s : Set E} (h : Bornology.IsBounded s) :
    Bornology.IsVonNBounded 𝕜 s := by
  rcases h.subset_ball 0 with ⟨r, hr⟩
  rw [Metric.nhds_basis_ball.isVonNBounded_iff]
  rw [← ball_normSeminorm 𝕜 E] at hr ⊢
  exact fun ε hε ↦ ((normSeminorm 𝕜 E).ball_zero_absorbs_ball_zero hε).mono_right hr

Metric Boundedness Implies Von Neumann Boundedness in Normed Spaces

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$. If a subset $s \subseteq E$ is bounded in the metric sense (i.e., has finite diameter), then $s$ is von Neumann bounded (i.e., every neighborhood of zero absorbs $s$).

NormedSpace.isVonNBounded_ball theorem

(r : ℝ) : Bornology.IsVonNBounded 𝕜 (Metric.ball (0 : E) r)

Full source

theorem isVonNBounded_ball (r : ℝ) : Bornology.IsVonNBounded 𝕜 (Metric.ball (0 : E) r) :=
  isVonNBounded_of_isBounded _ Metric.isBounded_ball

Open Balls are Von Neumann Bounded in Normed Spaces

Informal description

For any real number $r > 0$, the open ball $B(0, r) = \{x \in E \mid \|x\| < r\}$ in a normed space $E$ over a field $\mathbb{K}$ is von Neumann bounded. That is, every neighborhood of zero in $E$ absorbs $B(0, r)$.

NormedSpace.isVonNBounded_closedBall theorem

(r : ℝ) : Bornology.IsVonNBounded 𝕜 (Metric.closedBall (0 : E) r)

Full source

theorem isVonNBounded_closedBall (r : ℝ) :
    Bornology.IsVonNBounded 𝕜 (Metric.closedBall (0 : E) r) :=
  isVonNBounded_of_isBounded _ Metric.isBounded_closedBall

Closed Balls are Von Neumann Bounded in Normed Spaces

Informal description

For any real number $r > 0$, the closed ball $\overline{B}(0, r) = \{x \in E \mid \|x\| \leq r\}$ in a normed space $E$ over a field $\mathbb{K}$ is von Neumann bounded. That is, every neighborhood of zero in $E$ absorbs $\overline{B}(0, r)$.

NormedSpace.isVonNBounded_iff theorem

{s : Set E} : Bornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s

Full source

theorem isVonNBounded_iff {s : Set E} : Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 s ↔ Bornology.IsBounded s := by
  refine ⟨fun h ↦ ?_, isVonNBounded_of_isBounded _⟩
  rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, hρ, hρball⟩
  rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
  specialize hρball a ha.le
  rw [← ball_normSeminorm 𝕜 E, Seminorm.smul_ball_zero (norm_pos_iff.1 <| hρ.trans ha),
    ball_normSeminorm] at hρball
  exact Metric.isBounded_ball.subset hρball

Equivalence of Von Neumann Boundedness and Metric Boundedness in Normed Spaces

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$. A subset $s \subseteq E$ is von Neumann bounded if and only if it is bounded in the metric sense (i.e., has finite diameter).

NormedSpace.isVonNBounded_iff' theorem

{s : Set E} : Bornology.IsVonNBounded 𝕜 s ↔ ∃ r : ℝ, ∀ x ∈ s, ‖x‖ ≤ r

Full source

theorem isVonNBounded_iff' {s : Set E} :
    Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 s ↔ ∃ r : ℝ, ∀ x ∈ s, ‖x‖ ≤ r := by
  rw [NormedSpace.isVonNBounded_iff, isBounded_iff_forall_norm_le]

Von Neumann Boundedness Criterion in Normed Spaces: $\exists r, \forall x \in s, \|x\| \leq r$

Informal description

A subset $s$ of a normed space $E$ over a field $\mathbb{K}$ is von Neumann bounded if and only if there exists a real number $r$ such that for every $x \in s$, the norm of $x$ satisfies $\|x\| \leq r$.

NormedSpace.image_isVonNBounded_iff theorem

 {α : Type*} {f : α → E} {s : Set α} : Bornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r

Full source

theorem image_isVonNBounded_iff {α : Type*} {f : α → E} {s : Set α} :
    Bornology.IsVonNBoundedBornology.IsVonNBounded 𝕜 (f '' s) ↔ ∃ r : ℝ, ∀ x ∈ s, ‖f x‖ ≤ r := by
  simp_rw [isVonNBounded_iff', Set.forall_mem_image]

Image of a Set is Von Neumann Bounded if and Only if the Function is Uniformly Bounded on the Set

Informal description

Let $E$ be a normed space over a field $\mathbb{K}$, and let $f : \alpha \to E$ be a function defined on a set $\alpha$. A subset $s \subseteq \alpha$ is such that the image $f(s)$ is von Neumann bounded in $E$ if and only if there exists a real number $r \geq 0$ such that for every $x \in s$, the norm of $f(x)$ satisfies $\|f(x)\| \leq r$.

NormedSpace.vonNBornology_eq theorem

: Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology

Full source

/-- In a normed space, the von Neumann bornology (`Bornology.vonNBornology`) is equal to the
metric bornology. -/
theorem vonNBornology_eq : Bornology.vonNBornology 𝕜 E = PseudoMetricSpace.toBornology := by
  rw [Bornology.ext_iff_isBounded]
  intro s
  rw [Bornology.isBounded_iff_isVonNBounded]
  exact isVonNBounded_iff _

Equality of von Neumann Bornology and Metric Bornology in Normed Spaces

Informal description

In a normed space $E$ over a field $\mathbb{K}$, the von Neumann bornology coincides with the metric bornology. That is, the collection of von Neumann bounded subsets of $E$ is equal to the collection of metrically bounded subsets of $E$.

NormedSpace.isBounded_iff_subset_smul_ball theorem

{s : Set E} : Bornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.ball (0 : E) 1

Full source

theorem isBounded_iff_subset_smul_ball {s : Set E} :
    Bornology.IsBoundedBornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.ball (0 : E) 1 := by
  rw [← isVonNBounded_iff 𝕜]
  constructor
  · intro h
    rcases (h (Metric.ball_mem_nhds 0 zero_lt_one)).exists_pos with ⟨ρ, _, hρball⟩
    rcases NormedField.exists_lt_norm 𝕜 ρ with ⟨a, ha⟩
    exact ⟨a, hρball a ha.le⟩
  · rintro ⟨a, ha⟩
    exact ((isVonNBounded_ball 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Metric Boundedness via Scalar Multiplication of Unit Ball

Informal description

A subset $s$ of a normed space $E$ over a field $\mathbb{K}$ is bounded (in the metric sense) if and only if there exists a scalar $a \in \mathbb{K}$ such that $s$ is contained in the dilation of the unit ball centered at zero, i.e., $s \subseteq a \cdot B(0, 1)$.

NormedSpace.isBounded_iff_subset_smul_closedBall theorem

{s : Set E} : Bornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.closedBall (0 : E) 1

Full source

theorem isBounded_iff_subset_smul_closedBall {s : Set E} :
    Bornology.IsBoundedBornology.IsBounded s ↔ ∃ a : 𝕜, s ⊆ a • Metric.closedBall (0 : E) 1 := by
  constructor
  · rw [isBounded_iff_subset_smul_ball 𝕜]
    exact Exists.imp fun a ha => ha.trans <| Set.smul_set_mono <| Metric.ball_subset_closedBall
  · rw [← isVonNBounded_iff 𝕜]
    rintro ⟨a, ha⟩
    exact ((isVonNBounded_closedBall 𝕜 E 1).image (a • (1 : E →L[𝕜] E))).subset ha

Metric Boundedness via Scalar Multiplication of Closed Unit Ball

Informal description

A subset $s$ of a normed space $E$ over a field $\mathbb{K}$ is bounded (in the metric sense) if and only if there exists a scalar $a \in \mathbb{K}$ such that $s$ is contained in the dilation of the closed unit ball centered at zero, i.e., $s \subseteq a \cdot \overline{B}(0, 1)$.

Mathlib.Analysis.LocallyConvex.Bounded

Main declarations

Main results

References