Weak sequential compactness from uniform integrability
Abstract
Uniform integrability gives a genuinely weakly convergent real L1 subsequence over any finite measure.
RealLone(mu) denotes MeasureTheory.Lp Real 1 mu, and representatives(f) denotes its actual coerced representative sequence. The sigma algebra is arbitrary and the finite measure may be zero. No nonatomicity, countable generation, positivity or ambient separability is assumed.
Theorem 1.1 (A weak subsequence for every uniformly integrable real L1 sequence).
Proof. Machine-checked in Lean as D5/S3/Topology/Measures/L1UniformIntegrableWeak.exists_weak_subsequence (✓ std3). ∎
Source. Repository-derived.
Commentary.
Mathlib UniformIntegrable.spec supplies uniform hard-tail bounds at errors 1/(m+1). Restriction to the strict complementary level set gives bounded L2 functions. The inclusion L2 → L1 preserves the identical almost-everywhere class and is bounded by the finite-measure exponent comparison, including zero total measure. The common Hilbert approximation theorem therefore gives one increasing selector and an actual L1 limit, tested against every continuous real linear functional. This proves the weak-extraction part of the classical subsequence-splitting argument. It supplies neither the disjoint-carrier selection nor the signed-measure transfer or the full CH/Talagrand conclusion.