Represented weak-star subsequence compactness for signed measures
Abstract
Compact metric signed-measure sequences have represented weak-star subsequences with the same total-variation bound.
K is an arbitrary compact metric space with its Borel measurable structure. For every real C with 0 ≤ C and every sequence s of actual finite SignedMeasure K whose real total variation on univ is at most C, the theorem produces a strictly monotone subsequence and an actual SignedMeasure K limit with the same bound.
Theorem 1.1 (Actual signed-measure weak-star subsequence supplier).
Proof. Machine-checked in Lean as D5/S3/Topology/Measures/SignedWeakStarCompactness.exists_subsequence_tendsto_signedFunctional (✓ std3). ∎
Source. Repository-derived.
Commentary.
In the displayed statement, apply(f,x) means f(x). The first Tendsto argument is the pointwise sequence n ↦ toWeakDual(signedFunctional(s(phi(n)))), indexed by n : Nat. The source filter is atTop on Nat and the limit filter is nhds(toWeakDual(signedFunctional(mu))). totalVariationRealUniv(t) means t.totalVariation.real univ.
The proof writes each signed measure as the difference of its actual Jordan positive and negative finite measures. The pairs with summed mass at most C form a closed subset of the product of two compact finite-measure mass balls, using the pinned Prokhorov compactness theorem and continuity of mass.
The pair-to-functional map is continuous because evaluation at each continuous real test function is the difference of the two continuous finite-measure integrals. Its compact image in the weak dual is metrizable because C(K,Real) is separable for compact metric K. Sequential compactness of the image therefore supplies a strictly monotone subsequence and a point still represented by a finite-measure pair.
The represented limit is the difference of that pair. Vector-measure variation_sub_le and the Jordan mass identity give total variation at most the original C, including C=0 and signed measures of either sign. No Nonempty K, positivity, probability normalization, finite support, or zero-dimensional hypothesis is used; empty K remains covered.
This supplier only provides the reference represented weak-star limit for compact metric successor stages. It does not construct norm-preserving lifts, settle the CH scheduler or recursion, extend to the nonmetrizable final layer, or solve Problem 8.2.