Alphabeta Math
LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedaudited 2026-09-14
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 0s,t and a real random variable XtXs has law N(0,ts), then, for every integer m1, EXtXs2m=cmtsm, where cm=EZ2m=(2m1)!!=13(2m1)< for ZN(0,1). In particular, when m2, this is the moment hypothesis of the one-parameter Kolmogorov criterion with α=2m, β=m1, and CT=cm.

Facts & Assumptions

Given: Times s,t0, the stated increment law, and an integer m1.

[F1]

Under AC, N(0,1) is the probability measure with density ϕ(x)=ex2/2/2π, and N(0,h) is its image under xhx, including h=0. Standard normal and normal laws The Axiom of Choice

[F2]

A nonnegative expectation is the integral of the corresponding function against the random variable's law. Change of variables for expectation

[F3]

Integration against the measure with density ϕ equals integration of the product with ϕ against Lebesgue measure. Integrating against a density agrees with integrating the product

[F4]

Increasing nonnegative measurable functions may be passed to the limit under the integral. Monotone convergence for the integral

[F5]

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 u,v are differentiable on [a,b] with u,v integrable, then abuv=u(b)v(b)u(a)v(a)abuv A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral

[F7]

The exponential is its nonnegative power series, so for R>0 and every integer k0, eR2/2(R2/2)k/k!. The power-series, product-limit, IVP, functional-equation, and Picard definitions agree

Proof

technique · direct
1.1

Let Z be the coordinate map on the canonical N(0,1) probability space. By [F1]--[F3], for each integer r0, EZ2r=Rx2rϕ(x)dx, with either side initially allowed to be infinite.

F1F2F3
1.2

For an integer R1 and r1, [F5] on [R,R], applied to u(x)=x2r1 and v(x)=ϕ(x), is legitimate by [F6] and gives RRx2rϕ(x)dx=2R2r1ϕ(R)+(2r1)RRx2r2ϕ(x)dx. The sign and factor two come from the odd power at the two endpoints and the evenness of ϕ.

F5F6algebra
2.1

Taking k=r+1 in [F7] shows 0R2r1ϕ(R)2r+1(r+1)!2πR30. 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 ϕ=1 from [F1] yield recursively c0=1,cr=(2r1)cr1. Thus cm=(2m1)!! and every cm is finite.

step 1.1step 1.2F1F4F5F7algebra
3.1

Put h=ts. By [F1], the law N(0,h) is that of hZ; applying [F2] to the nonnegative function xx2m and using step 2.1 gives EXtXs2m=EhZ2m=hmcm. This includes h=0, when both sides vanish and the law is the Dirac mass at zero.

givenstep 2.1F1F2algebra
4.1

If m2, set α=2m and β=m1>0. Then m=1+β, so step 3.1 reads EXtXsα=cmts1+β. The constant CT=cm is finite and independent of T. 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.

step 2.1step 3.1F1algebra

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

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