Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Levy characterization of Brownian motion

Statement

Assume the Axiom of Choice. Let (Ω,F,P) be a probability space with a continuous-time filtration (Ft)t0, and let M be a real continuous local martingale relative to (Ft) with M0=0 almost surely and quadratic variation [M]t=t for every t0 in the sense of Quadratic covariation of Brownian Ito processes. Then M is a standard Brownian motion Brownian motion and satisfies the standing hypothesis (H) of Elementary predictable Brownian integrands relative to (Ft): M is adapted, has continuous paths, and for all 0s<t the increment MtMs is independent of Fs with law N(0,ts).

Facts & Assumptions

Given: AC, a filtered probability space with continuous-time filtration (Ft), a real continuous local martingale M with M0=0 almost surely and [M]t=t for all t, and times 0s<t.

[F1]

Characteristic exponential. The lemma Characteristic exponential for a continuous local martingale with deterministic clock gives, for every real θ, the conditional identity E[eiθ(MtMs)Fs]=eθ2(ts)/2 almost surely, together with the complex martingale property of exp(iθMt+θ2t/2). Characteristic exponential for a continuous local martingale with deterministic clock Continuous-time adapted processes and martingales

[F2]

Gaussian law and its characteristic function. For σ2>0 the law N(0,σ2) is defined as the pushforward of N(0,1) under xσx, and its characteristic function is ϕ(θ)=eθ2σ2/2: the computation is the direct Gaussian density computation eiθx(2πσ2)1/2ex2/(2σ2)dx=eθ2σ2/2; the value θ=0 gives 1. Standard normal and normal laws The standard normal density has total mass one

[F3]

Uniqueness from characteristic functions. Two Borel probability laws on R with equal characteristic functions are equal. Uniqueness of a law from its characteristic function

[F4]

Conditional expectations and test events. Conditional expectations are unique almost-sure classes, and for AFs the identity E[1AXFs]=1AE[XFs] holds; the tower property gives E[1AE[XFs]]=E[1AX]. Conditional expectation as an ae class Tower property of conditional expectation

[F5]

AC bookkeeping. Choice is declared for the conditional-expectation interface. The Axiom of Choice

Proof

technique · direct
1.1

The conditional law of the increment is N(0,ts): by [F1], E[eiθ(MtMs)Fs]=eθ2(ts)/2 for every real θ; for each AFs, [F4] gives E[1Aeiθ(MtMs)]=E[1A]eθ2(ts)/2. Let QA(Γ):=E[1A1{MtMsΓ}] for Borel Γ, a finite measure of total mass P(A); its Fourier transform is QA's transform E[1Aeiθ(MtMs)]=P(A)ϕts(θ) with ϕts the characteristic function of N(0,ts) by [F2]. Since QA and P(A)N(0,ts)() are finite Borel measures with equal Fourier transforms, [F3] applied after normalization (or to the differences) gives QA(Γ)=P(A)N(0,ts)(Γ) for all Borel Γ.

F2F3F4
2.1

Independence: taking A=Ω in step 1.1 gives the marginal law P(MtMsΓ)=N(0,ts)(Γ). For general AFs and Borel Γ, step 1.1 therefore gives E[1A1{MtMsΓ}]=P(A)P(MtMsΓ), which is exactly the independence of MtMs from Fs, together with the stated law.

F3step 1.1
3.1

Finite lists of increments: for 0=t0<t1<<tn the increments MtjMtj1 are independent with laws N(0,tjtj1). Induction on n: for n=1 this is step 2.1; given the claim for n increments, the conditional law of the increment at tn+1 given Ftn is N(0,tn+1tn) by step 2.1 and is independent of Ftn, hence independent of the sigma-algebra generated by the previous increments (which is contained in Ftn), and the tower property [F4] multiplies the joint law.

F4step 2.1
4.1

Conclusion and boundary cases: M is adapted, has continuous paths and M0=0 almost surely, and steps 2.1 and 3.1 verify clauses 2 and 3 of the definition of a standard Brownian motion and the increment condition (H) relative to (Ft); hence M is a standard Brownian motion with the stated filtration property. At s=t the increment is 0 with law N(0,0) and independence is trivial; at s=0 the identity gives the law of Mt; for θ=0 the conditional identity is the trivial constant-1 identity; if the clock were ct with c>0, rescaling would give the Gaussian factor ecθ2(ts)/2 and the same argument with variance c(ts); a non-continuous local martingale is not covered, since continuity is used both from the lemma and in the definition of Brownian motion; and AC enters only through [F5].

F1F5step 3.1

Source notes

Van der Vaart, Theorem 6.1, characterizes Brownian motion by the characteristic exponential of a continuous local martingale with quadratic variation t. The conditional-law argument of steps 1.1--2.1 is the standard characteristic-function uniqueness route; the conditional expectation is used only through event-testing, so no regular conditional distribution is introduced.

Depends on

Used by

Nothing in the library uses this result yet.

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