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.
A deterministic integral construction of a Gaussian process
Example
Assume the Axiom of Choice. Let be a standard Brownian motion and fix the measurable probability-one event from its continuity clause. Define the zero-repaired pathwise integral
where the integral on is the deterministic Riemann integral. Then is a centered Gaussian process and
For , this covariance equals
Facts & Assumptions
Given: AC, a standard Brownian motion , and its specified measurable probability-one continuity event .
Brownian motion is a centered Gaussian process with covariance , and every path indexed by is continuous. Brownian motion, Gaussian process.
Finite arithmetic combinations and sequential pointwise limits of measurable real functions are measurable. Arithmetic and lattice operations preserve measurability whenever they are defined, Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable.
A continuous function on a compact interval is Riemann integrable, and all tagged sums with mesh tending to zero converge to its integral. A continuous function on is Riemann integrable, by Heine-Cantor and Riemann's criterion, The Darboux and Riemann definitions agree: a bounded on is Darboux integrable with integral if and only if for every real there is a real such that for every tagged partition of mesh below .
A continuous function on a nondegenerate compact rectangle is Riemann integrable, all tagged product-grid sums converge with mesh, and its multiple integral equals either ordinary iterated integral. Every continuous function on a closed nondegenerate rectangle in is Riemann integrable, The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree, Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections.
Covariance is bilinear in finite linear combinations. Covariance is symmetric and bilinear in finite linear combinations.
Characteristic functions are expectations of complex exponentials; has characteristic function and the specified mean and variance. Characteristic function of a real random variable, Characteristic function of a normal law.
Dominated convergence applies to integrable complex random variables, and for real . Dominated convergence, , , and .
Under AC, a real probability law is determined by its characteristic function, and exists for every , including . Uniqueness of a law from its characteristic function, Standard normal and normal laws.
The fundamental theorem, the derivative power rule, and derivative algebra evaluate the compact polynomial integrals used below. The second fundamental theorem: if is differentiable on with and is integrable, then , For a natural the function is differentiable everywhere with derivative ; for it is the constant , with derivative ; for a natural the function is differentiable at every with derivative ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term, Sums, scalar multiples, products and quotients: , , , and when .
AC is used through the Brownian, deterministic-integration, normal-law, and characteristic-function uniqueness suppliers. The Axiom of Choice.
Verification
For and , put This is a measurable random variable by [F2]. On , [F3] makes converge to the displayed Riemann integral as ; for , every sum and the integral are zero. Define by this limit on and by zero on . It is measurable: the convergence set and limsup of the measurable sequence are measurable by [F2], and pasting that finite limit on the measurable set with zero on its complement preserves every Borel inverse image. Thus the statement defines a real stochastic process rather than an integral that might be undefined on exceptional paths.
For , covariance bilinearity and [F1] give This is the lower-corner product-grid Riemann sum for the continuous function on . Its mesh tends to zero, so [F4] gives If or , both and the declared degenerate-rectangle integral are zero, so the same conclusion holds.
Fix , times , coefficients , and set and . By [F1], is centered normal. Step 1.2 and covariance bilinearity show that its variance converges to On , step 1.1 gives , hence the convergence is almost sure. In particular, .
Now let . Every section of is continuous, so [F4] writes The polynomial antiderivatives justified by [F9] give For both the double integral and polynomial are zero by their endpoint conventions.
For each real , [F6] gives . The left side converges to by [F7], because almost surely and every modulus is one; the right side converges to . By [F8], . Since the finite list and coefficients were arbitrary, is a centered Gaussian process. This argument proves Gaussian closure from the actual almost-sure Riemann-sum limit; it does not assume that arbitrary pointwise limits of Gaussian variables remain Gaussian.
Apply step 3.1 to the singleton coefficients and to . It gives and . Covariance bilinearity also gives . Comparing and cancelling proves , including or .
Steps 1.1--4.1 prove every claim. Repeated times, zero coefficients, and singular linear combinations are retained in steps 2.1 and 3.1; is handled without a nondegenerate rectangle, and the empty finite list has the unique empty-tuple law. Changing the chosen probability-one continuity event changes only on a null set for each , so the asserted finite laws and covariance are unaffected. AC is used exactly through [F1], [F3], [F6], and [F8], including the countable-choice input inherited by the continuous-integrability interface in [F3]; the fixed uniform left-endpoint sums, pasting, and finite algebra require no further choices.
Source notes
Yoshida, Section 6.1, Lemma 6.1.3 and equation (6.5), printed pp. 174--175, supplies the Gaussian finite-combination and Brownian covariance inputs; Section 6.3 supplies Brownian path regularity context. The zero repair, Riemann-sum characteristic-function passage, double-integral covariance, and polynomial evaluation are derived in full above.
Depends on
- Brownian motion
- Gaussian process
- Arithmetic and lattice operations preserve measurability whenever they are defined
- Sequential suprema, infima, limsup, liminf, and pointwise limits of measurable functions are measurable
- A continuous function on $[a,b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion
- The Darboux and Riemann definitions agree: a bounded $f$ on $[a,b]$ is Darboux integrable with integral $I$ if and only if for every real $\varepsilon > 0$ there is a real $\delta > 0$ such that $|S(f,P,\xi) - I| < \varepsilon$ for every tagged partition of mesh below $\delta$
- Every continuous function on a closed nondegenerate rectangle in $\mathbb{R}^m$ is Riemann integrable
- The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree
- Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections
- Covariance is symmetric and bilinear in finite linear combinations
- Characteristic function of a real random variable
- Characteristic function of a normal law
- Dominated convergence
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- Uniqueness of a law from its characteristic function
- Standard normal and normal laws
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- For a natural $n \ge 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $\iota(n)\,x^{\,n-1}$; for $n = 0$ it is the constant $1$, with derivative $0$; for a natural $n \ge 1$ the function $x \mapsto x^{-n}$ is differentiable at every $x \ne 0$ with derivative $-\iota(n)\,x^{-n-1}$; consequently every polynomial function is differentiable at every real, with the derivative computed term by term
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- The Axiom of Choice
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
131 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
- Nobuaki Yoshida, Probability Theory, Sections 6.1--6.3 (standard reference, not scraped)