Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Radial second moment of multidimensional Brownian motion

Example

Assume the Axiom of Choice. Let d1 be finite, let B=(Bt)t0 be a standard d-dimensional Brownian motion, and give it its uncompleted natural filtration

Ft=σ(Bu:0ut).

Then

EBt22=dt(t0),

and the real process

Mt=Bt22dt

is an all-pairs continuous-time martingale: for every 0st,

E[MtFs]=Msalmost surely.

Facts & Assumptions

Given: AC, a finite integer d1, and a standard d-dimensional Brownian motion B.

[F1]

A standard d-dimensional Brownian motion starts at zero almost surely, has mutually independent vector increments with law Nd(0,hId) on every finite increasing grid, and equivalently has independent standard scalar Brownian coordinate processes. d-dimensional Brownian motion

[F2]

The uncompleted natural filtration is generated by observations up to time t; an all-pairs martingale is adapted, integrable at each time, and satisfies the displayed conditional identity for every st. Continuous-time filtrations and all-pairs martingales

[F3]

Disjoint groups of independent sigma-algebras remain independent, and measurable functions applied separately to independent random elements remain independent. Disjoint groups of an independent sigma-algebra family remain independent Measurable coordinatewise functions preserve independence

[F4]

A pi-system contained in a lambda-system generates a sigma-algebra still contained in that lambda-system; probability is finitely additive and continuous on increasing event sequences. Dynkin's pi-lambda theorem Basic identities for a probability measure

[F6]

A scalar N(0,h) variable has mean zero and variance, hence second moment, h, including h=0. Characteristic function of a normal law

[F7]

A variable measurable for the conditioning sigma-algebra conditions to itself; an integrable variable independent of that sigma-algebra conditions to its mean. Conditional expectation is linear, and a finite known factor may be taken out when the products are integrable. Ordinary L1 integration is linear on arbitrary measure spaces. Conditioning a known variable and an independent variable Basic algebra and order properties of conditional expectation Taking out what is known The Lebesgue integral is linear on L1(μ)

[F8]

Products of square-integrable real variables are integrable by Cauchy--Schwarz. Cauchy-Schwarz for random variables

[F9]

AC is used through the Brownian, normal-law, and conditional-expectation suppliers. The Axiom of Choice

Verification

technique · direct
1.1

Write Bt=(Bt1,,Btd). By [F1], each Btα has law N(0,t), so [F6] gives E[(Btα)2]=t. The coordinate-square sum in [F5] and finite L1 linearity in [F7] therefore give EBt22=α=1dE[(Btα)2]=dt. Thus Bt22 and Mt are integrable. The map xx22 is continuous, hence Borel by [F5]; since Bt is an observation generating Ft, both Bt22 and Mt are Ft-measurable. Consequently M is adapted. At t=0, the same calculation gives expectation zero although B0=0 is only an almost-sure identity.

F1F2F5F6F7
1.2

Fix 0s<t and put Δ=BtBs. Let Πs consist of Ω and all finite intersections j=1m{BujAj},0ujs,AjB(Rd). It is a pi-system and its generated sigma-algebra is Fs by [F2]. Given one such cylinder, sort its distinct positive observation times and adjoin 0,s,t. On the probability-one event {B0=0}, every displayed past observation is a finite cumulative sum of the vector increments ending no later than s. Those increments and Δ are disjoint groups of the mutually independent increment family in [F1]; [F3] makes their grouped vectors, and then the past observation tuple and Δ, independent. Replacing the tuple by its almost-surely equal cumulative-sum expression changes the cylinder event by a null set, so for every Borel CRd and every AΠs, P(A{ΔC})=P(A)P(ΔC). Empty cylinders give Ω. If s=0, every finite past tuple is almost surely the constant zero tuple, and the same null-set argument gives the identity.

F1F2F3F9
2.1

Fix a Borel CRd and let ΛC be the events AFs satisfying the factorization in step 1.2. The class contains Ω; finite differences of nested members follow by subtracting the two finite probability identities, and increasing countable unions follow from probability continuity in [F4]. Thus ΛC is a lambda-system containing Πs. By [F4], it contains σ(Πs)=Fs. Since C was arbitrary, Δ is independent of Fs. For s=t, Δ=0 identically and the same independence conclusion is immediate.

step 1.2F4
3.1

Let h=ts0. By [F1], the coordinates of Δ have laws N(0,h); [F6] and [F7] give E[ΔαFs]=0,E[Δ22Fs]=EΔ22=dh. Indeed each scalar coordinate and the squared norm are Borel functions of the independent vector from step 2.1, and the squared norm is integrable by [F5]--[F7]. Also Bsα and Δα are square-integrable by [F1] and [F6], so [F8] makes their product integrable. Because Bsα is Fs-measurable, taking out what is known yields E[BsαΔαFs]=BsαE[ΔαFs]=0. The formulas also hold when h=0, where Δ=0 pointwise.

step 2.1F1F5F6F7F8
4.1

The pathwise Euclidean identity Bt22=Bs22+2α=1dBsαΔα+Δ22 and conditional linearity now give E[Bt22Fs]=Bs22+d(ts). Subtracting the deterministic dt proves E[MtFs]=Bs22+d(ts)dt=Ms. With the adaptation and integrability from step 1.1, this is exactly the all-pairs martingale definition in [F2].

step 1.1step 3.1F2F5F7algebra
5.1

Steps 1.1--4.1 prove both displayed claims. The case d=1 is Durrett's scalar square martingale; d=0 is excluded. Time zero, s=0, s=t, and t=0 are all covered, and no completed or right-continuously augmented filtration has been substituted for the stated natural filtration. There is no biconditional. AC is used only through [F1], [F6], and [F7]; the finite grid, pi-lambda promotion, and coordinate sum make no additional choices.

step 1.1step 1.2step 2.1step 3.1step 4.1F1F2F6F7F9

Source notes

Durrett, Section 7.5, Theorem 7.5.4 and its proof, printed p. 376, proves Bt2t is a martingale by expanding across the future centered increment and conditioning on the Brownian past. The proof above supplies the finite d-coordinate extension and proves from the increment definition and a pi-lambda argument that the future vector increment is independent of the uncompleted natural filtration.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

110 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