How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Portmanteau theorem
Statement
For Borel probabilities on a metric space S, the following are equivalent: (i) ; (ii) integrals converge for all bounded uniformly continuous real tests; (iii) for every closed F; (iv) for every open G; (v) for every Borel A with .
Facts & Assumptions
, so the distance to a fixed nonempty set is -Lipschitz: Let be a metric space (def-metric-space), let be nonempty and let . Then
with the distance to a nonempty set (def-metric-bounded-diameter). Thus the real-valued function changes by at most between and : it is -Lipschitz.
Dominated convergence: Let and be measurable complex-valued functions such that almost everywhere and almost everywhere for a single nonnegative measurable function with . Then , and hence
Proof
Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.
(i) implies (ii) because a uniformly continuous function is continuous. Suppose (ii), and let F be nonempty and closed. By F1, is bounded and uniformly continuous. Moreover . Thus for every m. F2 with majorant one gives (iii) as m tends to infinity. For F empty the inequality is zero<=zero.
For G open, apply (iii) to its closed complement and use to obtain (iv). Conversely the same complement calculation obtains (iii) from (iv). If A is a Borel continuity set, and . The open lower bound and closed upper bound therefore squeeze to , proving (v).
Assume (v), and fix a bounded continuous real f and >0. The disjoint level sets with number at most r for each positive integer r. Their union over r contains all positive-mass levels and is countable (each finite subset of the real line can be listed in increasing order). Choose finitely many increasing levels outside this countable set, with , and mesh below . Such levels exist in every open interval, since an interval is uncountable.
For , continuity of f gives , so (v) applies. The simple function satisfies everywhere. Therefore . The finite sum tends to zero, by step 1.3 and (v). Letting tend to zero proves (i), closing all equivalences.
Depends on
Used by
- Weak limits are unique Corollary
- A nontight sequence with no probability law subsequence limit Counterexample
- Dirac laws converge weakly exactly when their points converge Example
- Quantile coupling on the real line Example
- Countable compactly supported tests determine euclidean weak convergence Lemma
- Real cdf and bounded continuous definitions agree Lemma
- Continuous mapping theorem Theorem
- Converging together lemma Theorem
- Levy prokhorov metric metrizes weak convergence Theorem
- Prokhorov tightness theorem on polish spaces Theorem
- Skorokhod representation on polish spaces Theorem
Dependency tree · two levels
44 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- van Gaans, Theorem 3.2, pp. 7–9 (standard reference, not scraped)