Alphabeta Math
TheoremStatement: 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.

Portmanteau theorem

Statement

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.

Facts & Assumptions

[F1]

d(x,A)d(y,A)d(x,y), so the distance to a fixed nonempty set is 1-Lipschitz: Let (X,d) be a metric space (def-metric-space), let AX be nonempty and let x,yX. Then

d(x,A)d(y,A)d(x,y),

with d(,A) the distance to a nonempty set (def-metric-bounded-diameter). Thus the real-valued function ud(u,A) changes by at most d(u,v) between u and v: it is 1-Lipschitz.

[F2]

Dominated convergence: Let f and (fn) be measurable complex-valued functions such that fnf almost everywhere and fng almost everywhere for a single nonnegative measurable function g with gdμ<+. Then fL1(μ), fnfdμ0, and hence fndμfdμ.

Proof

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

1.1

(i) implies (ii) because a uniformly continuous function is continuous. Suppose (ii), and let F be nonempty and closed. By F1, fm(x)=max(0,1md(x,F)) is bounded and uniformly continuous. Moreover fm1F. Thus lim supnμn(F)fmdμ for every m. F2 with majorant one gives (iii) as m tends to infinity. For F empty the inequality is zero<=zero.

F1F2
1.2

For G open, apply (iii) to its closed complement and use μn(G)=1μn(SG) to obtain (iv). Conversely the same complement calculation obtains (iii) from (iv). If A is a Borel continuity set, AAA and μ(A)=μ(A)=μ(A). The open lower bound and closed upper bound therefore squeeze μn(A) to μ(A), proving (v).

givenalgebra
1.3

Assume (v), and fix a bounded continuous real f and η>0. The disjoint level sets with μ(f=t)1/r 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 t0<<tm outside this countable set, with t0<f, tm>f and mesh below η. Such levels exist in every open interval, since an interval is uncountable.

givenalgebra
2.1

For Aj={tj1f<tj}, continuity of f gives Aj{f=tj1}{f=tj}, so (v) applies. The simple function s=jtj11Aj satisfies fsη everywhere. Therefore fdμnfdμ2η+jtj1(μn(Aj)μ(Aj)). The finite sum tends to zero, by step 1.3 and (v). Letting η tend to zero proves (i), closing all equivalences.

step 1.3

Depends on

Used by

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