Let \(A\subseteq D\) be uniformly bounded (\(|f(t)|\le M\) for all \(f\in A\), \(t\in [0,1]\)) and have uniformly decaying modulus: for every \(\varepsilon {\gt}0\) there is \(\delta \in (0,1)\) with \(w'_f(\delta ){\lt}\varepsilon \) for all \(f\in A\). Then \(A\) is totally bounded (an explicit finite net of rational step functions is constructed), and hence, by completeness, \(\overline{A}\) is compact. Only the sufficiency direction of Billingsley’s Theorem 12.3 is formalized; it is the direction consumed by tightness.

Let \(S\) be a set of measures on \(D\) such that (i) for every \(\eta {\gt}0\) there is \(a\) with \(\mu \{ f: a\le \operatorname {supNorm} f\} \le \eta \) for all \(\mu \in S\), and (ii) for all \(\varepsilon {\gt}0\) and \(\eta {\gt}0\) there is \(\delta \in (0,1)\) with \(\mu \{ f:\varepsilon \le w'_f(\delta )\} \le \eta \) for all \(\mu \in S\). Then \(S\) is tight (IsTightMeasureSet), with compact sets supplied by Theorem 6.9. Notably, no measurability of the sup-norm or modulus level sets is used — only monotonicity and countable subadditivity of measures — so downstream applications may bound the (outer) mass of the modulus level sets by that of any measurable superset.