Von Neumann Boundedness #
This file defines natural or von Neumann bounded sets and proves elementary properties.
Main declarations #
Bornology.IsVonNBounded: A setsis von Neumann-bounded if every neighborhood of zero absorbss.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 setSis bounded if and only if for any sequencex : ℕ → S,ε • xtends 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)
:
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 ∈ nhds 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 : Filter.HasBasis (nhds 0) q s)
:
Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (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 : Filter.HasBasis (nhds 0) q s)
:
Bornology.IsVonNBounded 𝕜 A ↔ ∀ (i : ι), q i → Absorbs 𝕜 (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.
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.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)
:
Bornology.IsVonNBounded 𝕜 (s + t)
theorem
Bornology.IsVonNBounded.neg
{𝕜 : Type u_1}
{E : Type u_3}
[SeminormedRing 𝕜]
[AddGroup E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[DistribMulAction 𝕜 E]
{s : Set E}
(hs : Bornology.IsVonNBounded 𝕜 s)
:
Bornology.IsVonNBounded 𝕜 (-s)
@[simp]
theorem
Bornology.isVonNBounded_neg
{𝕜 : Type u_1}
{E : Type u_3}
[SeminormedRing 𝕜]
[AddGroup E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[DistribMulAction 𝕜 E]
{s : Set E}
:
Bornology.IsVonNBounded 𝕜 (-s) ↔ Bornology.IsVonNBounded 𝕜 s
theorem
Bornology.IsVonNBounded.of_neg
{𝕜 : Type u_1}
{E : Type u_3}
[SeminormedRing 𝕜]
[AddGroup E]
[TopologicalSpace E]
[TopologicalAddGroup E]
[DistribMulAction 𝕜 E]
{s : Set E}
:
Bornology.IsVonNBounded 𝕜 (-s) → Bornology.IsVonNBounded 𝕜 s
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)
:
Bornology.IsVonNBounded 𝕜 (s - 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) (Filter.smallSets (nhds 0))
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 𝕜 S → Filter.Tendsto (fun (x : 𝕜) => x • S) (nhds 0) (Filter.smallSets (nhds 0))
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)}
:
Bornology.IsVonNBounded 𝕜 S ↔ ∀ (i : ι), Bornology.IsVonNBounded 𝕜 (Function.eval i '' S)
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)
:
Bornology.IsVonNBounded 𝕜 {x}
Singletons are bounded.
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)
:
Bornology.IsVonNBounded 𝕜 (x +ᵥ s)
@[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)
:
Bornology.IsVonNBounded 𝕜 (x +ᵥ s) ↔ Bornology.IsVonNBounded 𝕜 s
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 : Set.Nonempty s)
:
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 : Set.Nonempty t)
:
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 : Set.Nonempty s)
(ht : Set.Nonempty t)
:
Bornology.IsVonNBounded 𝕜 (s + t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
theorem
Bornology.isVonNBounded_add
{𝕜 : Type u_1}
{E : Type u_3}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[ContinuousSMul 𝕜 E]
[ContinuousAdd E]
{s : Set E}
{t : Set E}
:
Bornology.IsVonNBounded 𝕜 (s + t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
@[simp]
theorem
Bornology.isVonNBounded_add_self
{𝕜 : Type u_1}
{E : Type u_3}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[ContinuousSMul 𝕜 E]
[ContinuousAdd E]
{s : Set E}
:
Bornology.IsVonNBounded 𝕜 (s + s) ↔ Bornology.IsVonNBounded 𝕜 s
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 : Set.Nonempty t)
:
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 : Set.Nonempty s)
:
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 : Set.Nonempty s)
(ht : Set.Nonempty t)
:
Bornology.IsVonNBounded 𝕜 (s - t) ↔ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
theorem
Bornology.isVonNBounded_sub
{𝕜 : Type u_1}
{E : Type u_3}
[NormedField 𝕜]
[AddCommGroup E]
[Module 𝕜 E]
[TopologicalSpace E]
[ContinuousSMul 𝕜 E]
[TopologicalAddGroup E]
{s : Set E}
{t : Set E}
:
Bornology.IsVonNBounded 𝕜 (s - t) ↔ s = ∅ ∨ t = ∅ ∨ Bornology.IsVonNBounded 𝕜 s ∧ Bornology.IsVonNBounded 𝕜 t
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]
:
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
- Bornology.vonNBornology 𝕜 E = Bornology.ofBounded (setOf (Bornology.IsVonNBounded 𝕜)) ⋯ ⋯ ⋯ ⋯
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 : ℝ)
:
Bornology.IsVonNBounded 𝕜 (Metric.ball 0 r)
theorem
NormedSpace.isVonNBounded_closedBall
(𝕜 : 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)
:
theorem
NormedSpace.isVonNBounded_iff'
(𝕜 : Type u_1)
(E : Type u_3)
[NontriviallyNormedField 𝕜]
[SeminormedAddCommGroup E]
[NormedSpace 𝕜 E]
(s : Set E)
:
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')
:
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