Weak boundedness and norm boundedness

In a real or complex seminormed space, a set is norm bounded if and only if every continuous linear functional has bounded image on it. Equivalently, its image in WeakSpace is von Neumann bounded. In particular, weakly compact sets, weakly convergent sequences, and sets in which every sequence has a weakly convergent subsequence are norm bounded. No completeness or separability assumption on the original space is needed.

The proof applies Mathlib's banach_steinhaus to the evaluation functionals on the complete continuous dual, then uses NormedSpace.inclusionInDoubleDualLi to recover the original norms. Weak boundedness uses Bornology.IsVonNBounded, rather than a metric bornology on the weak topology.

References

• R. E. Megginson, An Introduction to Banach Space Theory, §2.5 (weak topologies).

theorem TauCeti.NormedSpace.isBounded_iff_forall_dual_isBounded (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : Bornology.IsBounded s ↔ ∀ (f : StrongDual 𝕜 E), Bornology.IsBounded (⇑f '' s)

A set is norm bounded exactly when all its continuous linear functional images are bounded. The space itself need not be complete.

@[simp]

theorem TauCeti.NormedSpace.isVonNBounded_toWeakSpace_iff (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : Bornology.IsVonNBounded 𝕜 (⇑(toWeakSpace 𝕜 E) '' s) ↔ Bornology.IsBounded s

A set is bounded for the weak topology exactly when it is norm bounded.

theorem IsCompact.isBounded_toWeakSpace_preimage {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set (WeakSpace 𝕜 E)} (hs : IsCompact s) : Bornology.IsBounded (⇑(toWeakSpace 𝕜 E) ⁻¹' s)

A weakly compact set is norm bounded, even in an incomplete space.

theorem Filter.Tendsto.isBounded_range_of_toWeakSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {u : ℕ → E} {x : E} (hu : Tendsto (fun (n : ℕ) => (toWeakSpace 𝕜 E) (u n)) atTop (nhds ((toWeakSpace 𝕜 E) x))) : Bornology.IsBounded (Set.range u)

A weakly convergent sequence is norm bounded, even in an incomplete space.

theorem TauCeti.isBounded_of_forall_tendsto_subseq_toWeakSpace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] {K : Set E} (hK : ∀ (u : ℕ → E), (∀ (n : ℕ), u n ∈ K) → ∃ (x : E) (σ : ℕ → ℕ), StrictMono σ ∧ Filter.Tendsto (fun (n : ℕ) => (toWeakSpace 𝕜 E) (u (σ n))) Filter.atTop (nhds ((toWeakSpace 𝕜 E) x))) : Bornology.IsBounded K

A set with weakly convergent subsequences for all its sequences is norm bounded. Subsequential limits need not belong to the set.