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.
Real cdf and bounded continuous definitions agree
Statement
For real random variables, the CDF continuity-point definition of convergence in distribution agrees with weak convergence of their laws.
Facts & Assumptions
Portmanteau theorem: 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 .
Convergence in distribution for real random variables: For real random variables and , write , or in distribution, when at every continuity point of . Here is the CDF from def-cumulative-distribution-function-of-a-random-variable and continuity points are those of def-atom-and-continuity-point-of-a-law.
Continuity from above when one set has finite measure: Let be a decreasing sequence of measurable sets for a measure . If for some , then
Continuity from below for measures: Let be an increasing sequence of measurable sets for a measure , so . Then
No finiteness hypothesis is required.
Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: Let with , let be the set of functions and let be the Euclidean metric on it (lem-metrics-on-rn). Then:
- Closed boxes are compact. For reals the box is a compact subset of (def-metric-compactness).
- Heine-Borel. A subset is a compact subset of if and only if is closed in (def-metric-topology) and bounded (def-metric-bounded-diameter).
- The real line. A subset is a compact subset of , the usual metric (lem-real-line-is-a-metric-space), if and only if is closed in and bounded.
No choice principle is used. The bisection below halves one coordinate at a time and takes the left half whenever the left half still fails to be finitely covered, the right half otherwise: a rule with two outcomes, decided by a property of the box, not a selection. That is the whole reason the theorem is available in ZF, while the general "complete and totally bounded implies compact" (thm-complete-and-totally-bounded-implies-compact) is not.
The hypothesis is inherited from lem-metrics-on-rn, which defines and its metrics only there; the last remark below records what happens at .
Proof
Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.
Use F4 for increasing rays. Use F3 for decreasing rays and intervals of finite probability. For a probability law , write . Continuity from above and below of finite measures show F is right-continuous, has limits zero and one at the two infinities, and has jump at t. Thus a continuity point has . If , F1 on gives at every such point, exactly F2.
Conversely assume convergence of CDFs at continuity points of F. Fix bounded continuous f, , and >0. Choose continuity points a<b with . They exist because tails tend to zero and the positive jumps form a countable set: at most r atoms have mass at least 1/r. CDF convergence makes the same sum of two tails less than 2eta for all large n.
The closed bounded interval is compact by F5. On [a,b], continuity is uniform: for each point choose a neighborhood on which oscillation is small, extract a finite subcover by compactness, and use the minimum of the finitely many smaller radii. Choose a finite partition by continuity points with oscillation of f on each interval below . Then converges to the corresponding mass. Integrals of the finite step approximation therefore converge. Its error inside (a,b] is at most for each law; the outside error is at most in the comparison of the two integrals, by step 1.2. Let decrease to zero. This proves weak convergence.
Depends on
- Portmanteau theorem
- Convergence in distribution for real random variables
- Continuity from above when one set has finite measure
- Continuity from below for measures
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
Used by
Nothing in the library uses this result yet.
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
- Durrett, Theorem 3.2.9, pp. 119–120 (standard reference, not scraped)