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.
Gaussian even moments for Brownian increments
Statement
Assume the Axiom of Choice. If and a real random variable has law , then, for every integer , where for . In particular, when , this is the moment hypothesis of the one-parameter Kolmogorov criterion with , , and .
Facts & Assumptions
Given: Times , the stated increment law, and an integer .
Under AC, is the probability measure with density , and is its image under , including . Standard normal and normal laws The Axiom of Choice
A nonnegative expectation is the integral of the corresponding function against the random variable's law. Change of variables for expectation
Integration against the measure with density equals integration of the product with against Lebesgue measure. Integrating against a density agrees with integrating the product
Increasing nonnegative measurable functions may be passed to the limit under the integral. Monotone convergence for the integral
Compact-interval integration by parts includes its two endpoint terms. Under countable choice, a bounded Riemann-integrable function on a compact interval is Lebesgue integrable there with the same integral. If are differentiable on with integrable, then A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
The power, product, and chain rules, together with , give . 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 The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with The exponential function is smooth and
The exponential is its nonnegative power series, so for and every integer , . The power-series, product-limit, IVP, functional-equation, and Picard definitions agree
Proof
Let be the coordinate map on the canonical probability space. By [F1]--[F3], for each integer , with either side initially allowed to be infinite.
For an integer and , [F5] on , applied to and , is legitimate by [F6] and gives The sign and factor two come from the odd power at the two endpoints and the evenness of .
Taking in [F7] shows The compact bridge in [F5] identifies every Riemann integral in step 1.2 with the corresponding Lebesgue integral. The truncated nonnegative integrands then increase to their whole-line counterparts, so [F4], step 1.1, and from [F1] yield recursively Thus and every is finite.
Put . By [F1], the law is that of ; applying [F2] to the nonnegative function and using step 2.1 gives This includes , when both sides vanish and the law is the Dirac mass at zero.
If , set and . Then , so step 3.1 reads The constant is finite and independent of . AC is used through [F1], which supplies the normal-law probability measure, and through the countable-choice hypothesis of the compact bridge used in step 2.1; all truncations and the recurrence are canonical.
Source notes
Durrett, Section 7.1, printed p. 358, uses the finite even moments of a normal increment in the Brownian continuity argument. Steps 1.1--2.1 supply the full compact-truncation integration-by-parts calculation, including the boundary term and its limit.
Depends on
- Standard normal and normal laws
- Change of variables for expectation
- Integrating against a density agrees with integrating the product
- Monotone convergence for the integral
- If $u,v$ are differentiable on $[a,b]$ with $u',v'$ integrable, then $\int_a^b u v' = u(b)v(b)-u(a)v(a) - \int_a^b u'v$
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
- The power-series, product-limit, IVP, functional-equation, and Picard definitions agree
- The exponential function is smooth and $(\exp)'=\exp$
- The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g(c)$, then $f \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- 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$
- 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
- The Axiom of Choice
Used by
Dependency tree · two levels
74 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
- Rick Durrett, Probability: Theory and Examples, Section 7.1 (standard reference, not scraped)