Compactness of operator balls in the weak operator topology

Let E be a normed space and F a complete inner product space over ℝ or ℂ. This file proves that every closed norm ball of E →L[𝕜] F is compact in the weak operator topology, taken on Mathlib's copy E →WOT[𝕜] F (ContinuousLinearMapWOT.isCompact_image_ofCLM_closedBall), and hence that every norm-bounded set of operators has weak operator compact closure (ContinuousLinearMapWOT.isCompact_closure_image_ofCLM_of_isBounded).

The analytic input is ContinuousLinearMapWOT.exists_norm_le_tendsto_of_tendsto_inner: a family of operators that is eventually bounded in norm by r and whose matrix coefficients ⟪y, A x⟫ all converge has a weak operator limit, and that limit has norm at most r. The limiting coefficients form a sesquilinear form bounded by r, which the Riesz representation turns back into an operator. Compactness of a ball then follows by applying this to an ultrafilter: each coefficient ranges over a compact disc of scalars, so it converges along the ultrafilter.

Weak operator compactness of the unit ball is the operator analogue of the Banach–Alaoglu theorem. It gives weak operator cluster points of bounded nets of operators, and the compactness of the unit ball of a von Neumann algebra.

References

Kadison–Ringrose, Fundamentals of the Theory of Operator Algebras I, §5.1, for the weak operator compactness of the unit ball of B(H).

theorem ContinuousLinearMapWOT.exists_norm_le_tendsto_of_tendsto_inner {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {α : Type u_4} {l : Filter α} [l.NeBot] {f : α → E →L[𝕜] F} {r : ℝ} (hf : ∀ᶠ (a : α) in l, ‖f a‖ ≤ r) (hlim : ∀ (x : E) (y : F), ∃ (c : 𝕜), Filter.Tendsto (fun (a : α) => inner 𝕜 y ((f a) x)) l (nhds c)) : ∃ (T : E →L[𝕜] F), ‖T‖ ≤ r ∧ Filter.Tendsto (fun (a : α) => ofCLM (f a)) l (nhds (ofCLM T))

A family of operators that is eventually bounded in norm by r, and whose matrix coefficients ⟪y, f a x⟫ all converge, converges in the weak operator topology to an operator of norm at most r.

theorem ContinuousLinearMapWOT.isCompact_image_ofCLM_closedBall {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] (A : E →L[𝕜] F) (r : ℝ) : IsCompact (ofCLM '' Metric.closedBall A r)

Weak operator compactness of operator balls. Every closed norm ball of bounded operators from a normed space to a complete inner product space is compact in the weak operator topology.

theorem ContinuousLinearMapWOT.isCompact_closure_image_ofCLM_of_isBounded {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [InnerProductSpace 𝕜 F] [CompleteSpace F] {s : Set (E →L[𝕜] F)} (hs : Bornology.IsBounded s) : IsCompact (closure (ofCLM '' s))

A norm-bounded set of operators from a normed space to a complete inner product space has compact closure in the weak operator topology.