ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

The uniform empirical CDF converges to a Brownian bridge

Example

Assume the Axiom of Choice. Let $X_{i}$ be iid Uniform $[0, 1]$ , $F_{n} (t) = P_{n} ([0, t])$ , and $F (t) = t$ . The empirical process $G_{n} (t) = \sqrt{n} (F_{n} (t) - F (t))$ , $0 \leq t \leq 1$ , converges weakly in outer expectation in $ℓ^{\infty} ([0, 1])$ to the standard Brownian bridge: the tight centered Gaussian process $B$ with covariance $E [B (s) B (t)] = \min (s, t) - s t .$

Facts & Assumptions

Given: Iid Uniform $[0, 1]$ observations and the fixed- $P$ bracketing functional CLT.

[A1]

For $0 \leq t \leq 1$ , $P ([0, t]) = t$ and the envelope of $f_{t} = 1_{[0, t]}$ is $H \equiv 1$ , so $P H^{2} = 1$ .

[A2]

AC is the premise of the functional CLT [F4] and permits choosing one rational approximant from each of the countably many nonempty intervals used in step 1.1 (The Axiom of Choice).

[F1]

Empirical, centered, and Rademacher processes: $F_{n} (t) = P_{n} f_{t}$ and $G_{n} (f_{t}) = \sqrt{n} (P_{n} f_{t} - P f_{t})$ .

[F2]

Donsker classes and asymptotic equicontinuity: a $P$ -Donsker limit is a tight centered Gaussian bridge with covariance $P [(f - P f) (g - P g)]$ .

[F3]

Covering, packing, bracketing numbers, and metric entropy: bracket width in $L^{2} (P)$ is the $L^{2} (P)$ norm of the nonnegative endpoint difference.

[F4]

Functional central limit theorem by bracketing entropy: under pointwise measurability, a square-integrable envelope, and a finite fixed- $P$ normalized $L^{2} (P)$ bracketing entropy integral, the process converges in outer expectation to a tight Gaussian bridge.

[F5]

$Q$ is countably infinite: $Q$ is countable.

[F6]

Every subset of an at most countable set is at most countable: every subset of an at most countable set is at most countable.

[F7]

The rationals embed densely in the reals: between any two distinct real numbers there is a rational.

Verification

Given: The objects and facts above.

1.1A2F1F5F6F7construct

The class $F = {f_{t} : t \in [0, 1]}$ is pointwise measurable. Since $1 \in Q$ , the rational thresholds together with $1$ are indexed by $Q \cap [0, 1]$ , which is countable by [F5]–[F6]. For each fixed $t < 1$ , [A2] and [F7] give rationals $q_{k} \in Q \cap (t, \min (1, t + 1 / (k + 1)))$ for every integer $k \geq 0$ , so $q_{k} \to t$ from above and $f_{q_{k}} (x) \to f_{t} (x)$ for every $x \in [0, 1]$ . For $t = 1$ , use the constant sequence $q_{k} = 1$ . The envelope $H \equiv 1$ is measurable and square-integrable.

1.2A1F3choosealgebra

For an integer $m \geq 1$ , the $m$ brackets $[f_{j / m}, f_{(j + 1) / m}]$ have $L^{2} (P)$ width $\sqrt{1 / m}$ , since their endpoint difference is the indicator of an interval of length $1 / m$ . Thus for $0 < ϵ \leq 1$ , choosing $m = ⌈ ϵ^{- 2} ⌉$ gives $N_{[]} (ϵ, F, L^{2} (P)) \leq m$ .

2.1A1F1F3F4step 1.1step 1.2algebra

Consequently $\log N_{[]} (ϵ, F, L^{2} (P)) \leq \log (1 + ϵ^{- 2}) \leq \log 2 + 2 \log (1 / ϵ)$ for $0 < ϵ \leq 1$ . Since $\log (1 / ϵ) \leq 1 / ϵ$ , the square-root entropy is bounded by $\sqrt{\log 2} + \sqrt{2} ϵ^{- 1 / 2}$ , an integrable function on $(0, 1]$ . All hypotheses of [F4] hold.

3.1A1A2F2F4step 2.1∎

Applying [F4] gives a tight centered Gaussian limit. For $s, t \in [0, 1]$ , $P (f_{s} f_{t}) = P ([0, \min (s, t)]) = \min (s, t)$ and $P f_{s} P f_{t} = s t$ , so [F2] gives covariance $\min (s, t) - s t$ . This is precisely the defining covariance of the standard Brownian bridge stated in the example, proving the claimed limit. AC is carried from [F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

87 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

Jon A. Wellner, Empirical Processes: Theory and Applications, Chapter 1, §§1–2 and 7 (standard reference, not scraped)
David Pollard, Empirical Processes: Theory and Applications, Section 10 (standard reference, not scraped)