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.
Borel sigma-algebra of continuous path space is generated by coordinates
Statement
Put , give the uniform-on-compacts topology, and write . Then Here each expression on the right denotes the smallest sigma-algebra on making every displayed coordinate map measurable. No choice principle is used.
Facts & Assumptions
Given: The path space , its uoc metric , and its coordinate maps as in the Statement. Write for the sigma-algebra generated by all coordinates and for that generated by the nonnegative rational coordinates.
The uoc metric is and its topology is compact convergence. Uniform-on-compacts metric on continuous path space
A Borel sigma-algebra is generated by the open sets, and a family of sets has a unique smallest generated sigma-algebra. The Borel sigma-algebra of a topological space The sigma-algebra generated by a family of sets Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal
Countable suprema and pointwise limits of measurable real functions are measurable; finite sums, scalar multiples, positive parts, and absolute values preserve measurability. Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable Closure properties of measurable functions used by the integral
The rationals are countable and dense in the reals. There is a fixed bijection between and , recursion constructs nested finite codes, finite products of countable sets are countable, and a subset of a countable set is countable. is countably infinite The rationals embed densely in the reals The recursion theorem A product of two at most countable sets is at most countable Every subset of an at most countable set is at most countable
Closed bounded real intervals are compact, continuous real functions on them are uniformly continuous, and for every there is with . Heine-Borel in : with the Euclidean metric a subset of 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 Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous For every in a complete ordered field there is a natural with
Every nonnegative real has an integer part, and . The geometric-series formula controls every tail . Integer part: for every real there is exactly one integer with For the sequence is null, and for the sequence diverges to For , , and for the series diverges
Metric balls form a base for the metric topology. The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
Proof
Fix and choose an integer with . If , then implies and hence . Thus every is continuous, so it is Borel measurable. Minimality in [F2] gives .
Fix and put . Then and , so by [F6]. For every , continuity gives . Every is -measurable by definition, so [F3] makes measurable. Hence by minimality, and therefore .
Let be the family of paths which, for some integers , are affine on each interval for , take rational values at all grid points , and are constant after . This family is countable without choice. Indeed, fix bijections and . Nested use of codes every finite sequence of naturals by one natural (and repeated application of decodes it); composing entries with codes every finite rational sequence. A further finite nesting codes together with that sequence, giving a surjection from a subset of onto . Thus [F4] makes at most countable.
The family is uoc dense. Given and , use [F6] to choose with . By [F5], is uniformly continuous on ; choose so that the oscillation of over distances at most is less than . By rational density, choose rational with for the finitely many (finite induction, not a choice principle), and let interpolate these values and remain constant after . On a grid interval, convex interpolation and the triangle inequality give . Consequently This also covers and .
Fix . For , continuity and rational density give Enumerating that rational set, [F3] makes -measurable. The finite partial sums of the metric formula are measurable by [F3] and converge pointwise to , so this distance is measurable. Hence every metric ball, with an arbitrary center, belongs to .
The balls with and positive rational form a countable base: countability follows from [F4], while density from step 1.4 and the triangle inequality put such a ball around every point inside any prescribed open ball. For an open , let be the subfamily of these basic balls which are contained in . It is countable by [F4], every member belongs to by step 1.5, and . Thus every open set is in ; [F2] yields . Combining this with steps 1.1 and 1.2 proves all stated equalities. The zero path shows and are nonempty; singleton and zero-time coordinates cause no exception, and no countable family of nonempty sets was selected.
Source notes
Van der Vaart and Wellner use the standard fact that the Borel sigma-algebra on a separable continuous-function space is generated by evaluations. The proof above supplies the complete uoc and rational-coordinate argument, including an explicit choice-free countable basis.
Depends on
- Uniform-on-compacts metric on continuous path space
- The Borel sigma-algebra of a topological space
- The sigma-algebra generated by a family of sets
- Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal
- The evaluation map $e : C(X,Y) \times X \to Y$, $e(f,x) = f(x)$
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
- Closure properties of measurable functions used by the integral
- $\mathbb{Q}$ is countably infinite
- The rationals embed densely in the reals
- Integer part: for every real $x$ there is exactly one integer $m$ with $m \le x < m + 1$
- $\mathbb{N} \times \mathbb{N} \approx \mathbb{N}$
- The recursion theorem
- A product of two at most countable sets is at most countable
- Every subset of an at most countable set is at most countable
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{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
- Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- For $|r| < 1$, $\sum_{k \ge 0} r^k = 1/(1-r)$, and for $|r| \ge 1$ the series diverges
- For $|r| < 1$ the sequence $r^k$ is null, and for $|r| > 1$ the sequence $|r|^k$ diverges to $+\infty$
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
Used by
- Existence and scaling of d-dimensional Brownian motion Corollary
- Brownian scaling Theorem
- Uniqueness of Wiener measure Theorem
Dependency tree · two levels
129 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
- A. W. van der Vaart and J. A. Wellner, Weak Convergence and Empirical Processes, Section 1.3 (standard reference, not scraped)