Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-10
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

[F1]

Portmanteau theorem: For Borel probabilities μn,μ on a metric space S, the following are equivalent: (i) μnμ; (ii) integrals converge for all bounded uniformly continuous real tests; (iii) lim supnμn(F)μ(F) for every closed F; (iv) lim infnμn(G)μ(G) for every open G; (v) μn(A)μ(A) for every Borel A with μ(A)=0.

[F2]

Convergence in distribution for real random variables: For real random variables (Xn) and X, write XnX, or XnX in distribution, when FXn(x)FX(x) at every continuity point x of FX. Here FX 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.

[F3]

Continuity from above when one set has finite measure: Let (En)nN be a decreasing sequence of measurable sets for a measure μ. If μ(En0)<+ for some n0, then

μ(nNEn)=infnNμ(En).

[F4]

Continuity from below for measures: Let (En)nN be an increasing sequence of measurable sets for a measure μ, so EnEn+1. Then

μ(nNEn)=supnNμ(En).

No finiteness hypothesis is required.

[F5]

Heine-Borel in Rn: with the Euclidean metric a subset of Rn 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 nN with n1, let Rn be the set of functions nR and let d2 be the Euclidean metric on it (lem-metrics-on-rn). Then:

  1. Closed boxes are compact. For reals akbk (k<n) the box Q={xRn:akxkbk for every k<n} is a compact subset of (Rn,d2) (def-metric-compactness).
  2. Heine-Borel. A subset KRn is a compact subset of (Rn,d2) if and only if K is closed in Rn (def-metric-topology) and bounded (def-metric-bounded-diameter).
  3. The real line. A subset KR is a compact subset of (R,dR), the usual metric dR(x,y)=xy (lem-real-line-is-a-metric-space), if and only if K is closed in R 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 n1 is inherited from lem-metrics-on-rn, which defines Rn and its metrics only there; the last remark below records what happens at n=0.

Proof

Given: The objects, hypotheses and definitions in the statement. Its conclusions are to be established below.

1.1

Use F4 for increasing rays. Use F3 for decreasing rays and intervals of finite probability. For a probability law μ, write F(t)=μ((,t]). 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 μ({t}) at t. Thus a continuity point has μ({t})=0. If μnμ, F1 on (,t] gives Fn(t)F(t) at every such point, exactly F2.

F1F2F3F4
1.2

Conversely assume convergence of CDFs at continuity points of F. Fix bounded continuous f, M=f, and η>0. Choose continuity points a<b with μ((,a])+μ((b,))<η. 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.

givenalgebra
2.1

The closed bounded interval [a,b] 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 a=t0<<tm=b by continuity points with oscillation of f on each interval below η. Then μn((tj1,tj])=Fn(tj)Fn(tj1) 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 3Mη in the comparison of the two integrals, by step 1.2. Let η decrease to zero. This proves weak convergence.

step 1.2F5

Depends on

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