LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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.

Cauchy sequences in probability have a measurable limit

Statement

Let $(Y_{n})_{n \geq 1}$ be real random variables on one probability space. Suppose that for every $ε, η > 0$ there is $N$ such that $P (∣ Y_{n} - Y_{m} ∣ > ε) < η (n, m \geq N) .$ Then there is a finite measurable real random variable $Y$ such that $Y_{n} \to Y$ in probability.

Facts & Assumptions

[F1]

Convergence in probability: For real random variables $(X_{n})$ and $X$ on one probability space, write $X_{n} \to X$ in probability when, for every $ε > 0$ , $P (∣ X_{n} - X ∣ > ε) ⟶ 0.$ This is precisely def-convergence-in-measure for the probability measure.

[F2]

First Borel-Cantelli lemma for events: Let $(A_{n})_{n \in N}$ be events in a probability space. If $\sum_{n = 0}^{\infty} P (A_{n}) < + \infty,$ then $P (A_{n} i . o .) = 0.$ No independence hypothesis is needed.

[F3]

A series converges iff for every $ε > 0$ there is $N$ with $∣ a_{m + 1} + \dots + a_{n} ∣ < ε$ for all $n > m \geq N$ : Let $(a_{k})$ be a sequence of reals, with partial sums $s_{n} = \sum_{k < n} a_{k}$ (def-series). Then $\sum a_{k}$ converges if and only if $for every real ε > 0 there is N \in N such that ∣ \sum_{k = m + 1}^{n} a_{k} ∣ < ε for all n > m \geq N .$ The block $\sum_{k = m + 1}^{n} a_{k}$ is the finite sum $a_{m + 1} + \dots + a_{n}$ of def-finite-sum, and it equals $s_{n + 1} - s_{m + 1}$ . This is the Cauchy criterion transported from sequences to series. Its value is that it decides convergence without producing, or even naming, the sum.

[F4]

Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable: Let $(X, A)$ be a measurable space and let $f_{n} : X \to \overline{R}$ be measurable for every $n \in N$ . Then the functions $\sup_{n} f_{n}, \inf_{n} f_{n}, {lim sup}_{n} f_{n}, {lim inf}_{n} f_{n}$ are measurable. The set ${x : \lim_{n} f_{n} (x) exists in \overline{R}}$ is measurable. In particular, if $f_{n} \to f$ pointwise, then $f$ is measurable.

[F5]

Almost-sure convergence implies convergence in probability: If $X_{n} \to X$ almost surely, then $X_{n} \to X$ in probability.

[F6]

Finite and countable subadditivity of measures: Let $μ$ be a measure and let $(E_{k})_{k \in N}$ be measurable. Then $μ (⋃_{k \in N} E_{k}) \leq \sum_{k = 0}^{\infty} μ (E_{k}) .$ For every $m \in N$ one also has $μ (⋃_{k < m} E_{k}) \leq \sum_{k < m} μ (E_{k}),$ including $m = 0$ , where both sides are $0$ .

Proof

Given: The objects and hypotheses of the statement.

1.1

Set $n_{0} = 1$ . For each $k \geq 1$ , choose recursively the least integer $n_{k} > n_{k - 1}$ for which all pairs of indices at least $n_{k}$ have probability less than $2^{- k}$ of separation exceeding $2^{- k}$ . Such an integer exists by the hypothesis. Thus, for every $k \geq 1$ , $P (∣ Y_{n_{k + 1}} - Y_{n_{k}} ∣ > 2^{- k}) < 2^{- k}$ . The first Borel–Cantelli lemma gives a measurable probability-one event where these inequalities fail only finitely often.

F2given

2.1

On that event the series of absolute successive differences is finite: its finite initial part is finite because all values are real, and its remaining part is bounded by a geometric series. Therefore the subsequence is Cauchy and has a finite real limit. Its finite convergence event is measurable: intersect the measurable extended-limit event with ${\sup_{k} ∣ Y_{n_{k}} ∣ < \infty}$ , a countable union of countable intersections. Define $Y$ to be this limit there and zero outside. The corresponding restricted sequence converges everywhere, so measurable limits give a real random variable.

F3F4step 1.1algebra

3.1

This subsequence converges almost surely and hence in probability to $Y$ . Fix $ε, η > 0$ , choose $N$ so late-pair errors at $ε / 2$ are below $η / 2$ , and then choose $k$ with $n_{k} \geq N$ and $P (∣ Y_{n_{k}} - Y ∣ > ε / 2) < η / 2$ . For all $n \geq N$ , the triangle and union bounds give $P (∣ Y_{n} - Y ∣ > ε) < η$ . This proves convergence of the full sequence, including constant sequences.

F5F6F1step 2.1givenalgebra∎

Depends on

Used by

Convergence in probability and almost surely agree for independent series Theorem

Dependency tree · two levels

28 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

Varadhan, Chapter 3, Exercise 3.11, p. 65 (standard reference, not scraped)