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.
Brownian time inversion
Statement
Assume the Axiom of Choice. If is standard Brownian motion, then defines another standard Brownian motion. In particular, its continuity at is part of the conclusion, not an inference from its finite-dimensional laws alone.
Facts & Assumptions
Given: AC and a standard Brownian motion with one probability-one continuity event .
Brownian motion is centered Gaussian with covariance and a common continuity event; conversely a centered Gaussian process with this covariance and such continuity is Brownian. Brownian motion Gaussian process Brownian covariance is equivalent to independent stationary normal increments
Two Gaussian processes with the same mean and covariance functions have equal finite-dimensional laws, including singular vectors and repeated indices. Mean and covariance determine Gaussian finite-dimensional laws
On an arbitrary product measurable space, finite-coordinate cylinders generate the cylinder sigma-algebra and form a pi-system. A measurable random element has a probability law. Coordinate maps, finite-coordinate cylinders, and the cylinder -algebra Finite-coordinate cylinders form a -system Random elements and real random variables The law of a random element is a probability measure
A lambda-system is closed under nested relative differences and increasing unions; measures are continuous from below; a lambda-system containing a pi-system contains its generated sigma-algebra. Lambda-systems, or Dynkin systems Continuity from below for measures Dynkin's pi-lambda theorem
The positive rationals are countable and dense, and for every there is with . is countably infinite The rationals embed densely in the reals For every in a complete ordered field there is a natural with
The intersection of two probability-one events has probability one. Basic identities for a probability measure
AC is inherited through the Gaussian and Brownian interfaces. The Axiom of Choice
Proof
For any finite positive times and coefficients , the linear combination is normal by [F1]. Appending any occurrences of only appends deterministic zero coordinates. Hence is a centered Gaussian process, including repeated-time and singular finite vectors.
For , If , both sides of the required identity are zero. Thus for all . By [F2], and have the same finite-dimensional laws.
Let and define by their coordinates. Each map is measurable for the cylinder sigma-algebra: the sets whose inverse images are measurable form a sigma-algebra containing every coordinate inverse image, hence all finite-coordinate cylinders and their generated sigma-algebra. Their pushforward laws are therefore probabilities by [F3]. Step 2.1 makes them equal on every finite-coordinate cylinder. The class of cylinder-measurable sets on which they agree is a lambda-system by normalization, nested finite differences, and continuity from below; [F3]--[F4] therefore give .
In put This is cylinder-measurable because all three index sets are countable by [F5]. The event has probability one by [F1] and [F6]. On , continuity of at zero gives , so . Equality from step 3.1 gives .
On , is continuous for every . Fix with and . Choose with by [F5], and then from the definition of . For every , fix an enumeration of the rationals and, for each integer , let be its least-indexed member of within of ; density in [F5] makes this canonical sequence converge to . Continuity gives . Since for all , we get . Therefore as . By [F6], the set of such has probability one, so has one common continuity event on .
Steps 1.1--2.1 give the centered Gaussian covariance characterization, and step 5.1 gives path continuity; [F1] therefore makes standard Brownian motion. The formula at is separately defined because is unavailable there. Empty finite lists are vacuous, singleton and repeated-time laws were included in step 1.1, and AC is used only through [F1]--[F2], not in the fixed countable rational argument.
Source notes
Sousi Theorem 6.7 and Yoshida Proposition 6.1.5 use equality of the rational finite-dimensional laws and positive-time continuity to obtain continuity at zero. Steps 3.1--5.1 spell out the intervening cylinder-law and measurable-event arguments.
Depends on
- Brownian motion
- Gaussian process
- Brownian covariance is equivalent to independent stationary normal increments
- Mean and covariance determine Gaussian finite-dimensional laws
- Coordinate maps, finite-coordinate cylinders, and the cylinder $\sigma$-algebra
- Finite-coordinate cylinders form a $\pi$-system
- Random elements and real random variables
- The law of a random element is a probability measure
- Lambda-systems, or Dynkin systems
- Continuity from below for measures
- Dynkin's pi-lambda theorem
- $\mathbb{Q}$ is countably infinite
- The rationals embed densely in the reals
- For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$
- Basic identities for a probability measure
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
75 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
- Perla Sousi, Advanced Probability, Theorem 6.7 (standard reference, not scraped)
- Nobuo Yoshida, Probability Theory, Proposition 6.1.5 and Lemmas 6.1.6--6.1.7 (standard reference, not scraped)