TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 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.

Converging together lemma

Statement

Let $X_{n}$ and $Y_{n}$ be Borel-measurable random elements with values in a metric space $S$ , on the same probability space for each $n$ , and let $X$ be an $S$ -valued Borel-measurable random element. Suppose $d (X_{n}, Y_{n})$ is measurable and $P (d (X_{n}, Y_{n}) > ε) \to 0$ for every $ε$ >0. If $X_{n} \Rightarrow X$ , then $Y_{n} \Rightarrow X$ .

Facts & Assumptions

[F1]

Portmanteau theorem: For Borel probabilities $μ_{n}, μ$ on a metric space S, the following are equivalent: (i) $μ_{n} \Rightarrow μ$ ; (ii) integrals converge for all bounded uniformly continuous real tests; (iii) ${lim sup}_{n} μ_{n} (F) \leq μ (F)$ for every closed F; (iv) ${lim inf}_{n} μ_{n} (G) \geq μ (G)$ for every open G; (v) $μ_{n} (A) \to μ (A)$ for every Borel A with $μ (\partial A) = 0$ .

[F2]

Continuity from above when one set has finite measure: Let $(E_{n})_{n \in N}$ be a decreasing sequence of measurable sets for a measure $μ$ . If $μ (E_{n_{0}}) < + \infty$ for some $n_{0}$ , then

$μ (⋂_{n \in N} E_{n}) = \inf_{n \in N} μ (E_{n}) .$

[F3]

$∣ d (x, A) - d (y, A) ∣ \leq 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 $A \subseteq X$ be nonempty and let $x, y \in X$ . Then

$∣ d (x, A) - d (y, A) ∣ \leq d (x, y),$

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

Proof

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

1.1

By F3, distance to nonempty $F$ is continuous; its sublevel sets are closed. For nonempty closed F put $F^{[ε]} = {x : d (x, F) \leq ε}$ , which is closed. If $Y_{n}$ lies in F and $d (X_{n}, Y_{n}) \leq ε$ , then $X_{n}$ lies in this enlargement. Thus $P (Y_{n} \in F) \leq P (X_{n} \in F^{[ε]}) + P (d (X_{n}, Y_{n}) > ε)$ .

givenalgebraF3

2.1

F1 and the probability hypothesis give ${lim sup}_{n} P (Y_{n} \in F) \leq P_{X} (F^{[ε]})$ . For $m \in N$ , the sets $E_{m} : = F^{[1 / (m + 1)]}$ decrease to F, so F2 makes their probabilities decrease to P_X(F). Empty F has probability zero without an enlargement. The resulting closed-set bound is again F1, now proving $Y_{n} \Rightarrow X$ .

F1F2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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 and closed-neighborhood argument (standard reference, not scraped)