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.

Countable compactly supported tests determine euclidean weak convergence

Statement

For each finite $d \geq 1$ there is a countable uniformly dense subset $D$ of $C_{c} (R^{d}; R)$ containing nonnegative compact cutoffs $χ_{m} ↑ 1$ . If Borel probabilities $μ_{n}, μ$ have $\int h d μ_{n} \to \int h d μ$ for every $h \in D$ , then $μ_{n} \Rightarrow μ$ .

Facts & Assumptions

[F1]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $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: Let $n \in N$ with $n \geq 1$ , let $R^{n}$ be the set of functions $n \to R$ and let $d_{2}$ be the Euclidean metric on it (lem-metrics-on-rn). Then:

Closed boxes are compact. For reals $a_{k} \leq b_{k}$ $(k < n)$ the box $Q = {x \in R^{n} : a_{k} \leq x_{k} \leq b_{k} for every k < n}$ is a compact subset of $(R^{n}, d_{2})$ (def-metric-compactness).
Heine-Borel. A subset $K \subseteq R^{n}$ is a compact subset of $(R^{n}, d_{2})$ if and only if $K$ is closed in $R^{n}$ (def-metric-topology) and bounded (def-metric-bounded-diameter).
The real line. A subset $K \subseteq R$ is a compact subset of $(R, d_{R})$ , the usual metric $d_{R} (x, y) = ∣ x - y ∣$ (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 $n \geq 1$ is inherited from lem-metrics-on-rn, which defines $R^{n}$ and its metrics only there; the last remark below records what happens at $n = 0$ .

[F2]

Monotone convergence for the integral: Let $0 \leq f_{1} \leq f_{2} \leq \dots$ be measurable and suppose $f_{n} (x) ↑ f (x)$ for every $x$ . Then $\int f_{n} d μ ↑ \int f d μ .$

[F3]

Weak convergence of borel probability measures: For Borel probability measures $μ_{n}, μ$ on a metric space S, write $μ_{n} \Rightarrow μ$ if $\int f d μ_{n} \to \int f d μ$ for every bounded continuous real function f on S. Continuity is def-metric-continuity. Such f is Borel measurable (inverse images of open sets are open) and $\int ∣ f ∣ d μ \leq ∥ f ∥_{\infty} μ (S) < \infty$ , so the integrals are finite in def-integrable-real-and-complex-functions-and-their-integrals. No completeness or coupling is required.

Proof

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

1.1

For each integer cube [-M,M]^d, take all finite rational rectangular grids and rational vertex values which are zero on every boundary vertex. Interpolate multilinearly in each grid rectangle and extend by zero outside the cube. Shared-face formulas agree because they use the same vertex data, and the outer face formulas vanish, so the extension is continuous and compactly supported. Finite rational data admit a countable enumeration, giving a countable family D.

givenalgebra

1.2

If f has compact support, F1 bounds its support inside the interior of some integer cube. Continuity on the cube is uniform: choose local oscillation neighborhoods, extract a finite subcover of smaller balls, and take a sufficiently small minimum radius. Thus choose a finite rational grid with f-oscillation below $η$ on every cell, and rational vertex values within $η$ of f, taking zero at boundary vertices. Multilinear interpolation is a convex combination of the vertex values. At a point x in any cell each vertex value differs from f(x) by less than 2eta, so the interpolant does too; outside the cube both functions vanish. This proves uniform density.

1.3

D contains $χ_{m} (x) = \prod_{j = 1}^{d} \min (1, \max (0, m + 1 - ∣ x_{j} ∣))$ : these are grid interpolants on [-m-1,m+1]^d, equal one on [-m,m]^d. They increase pointwise to one. F2 gives $\int χ_{m} d μ ↑ 1$ . Given $η$ >0 choose m with this integral greater than 1- $η$ . The assumed test convergence then gives $\int χ_{m} d μ_{n} > 1 - 2 η$ for all large n. Hence for K=[-m-1,m+1]^d the outside masses are at most $η$ for $μ$ and 2eta for late $μ_{n}$ .

2.1

Uniform density and the probability mass bound extend the assumed convergence to every compactly supported continuous test: approximate it within $δ$ by a D test, making the two integral errors at most 2delta. For any bounded continuous f, $f χ_{m + 1}$ is such a test and equals f on K. Therefore step 1.3 gives ${lim sup}_{n} ∣ \int f d μ_{n} - \int f d μ ∣ \leq 3 ∥ f ∥_{\infty} η$ . Let $η$ decrease to zero. This is F3.

F3step 1.3∎

Depends on

Used by

Empirical measures of iid euclidean samples converge weakly Theorem

Dependency tree · two levels

48 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, compact-test approximation in Proposition 5.3 and tightness transfer; explicit Euclidean construction (standard reference, not scraped)