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.

Blumenthal's zero-one law

Statement

Assume the Axiom of Choice, let B be a standard Brownian motion, and let F0+0 be the germ sigma-algebra at zero The Brownian germ sigma-algebra at zero. Then every event A∈F0+0 has P(A)∈{0,1}.

Facts & Assumptions

Given: AC, a standard Brownian motion B, and an event A∈F0+0.

[F1]

The germ sigma-algebra is the intersection of the raw pasts at positive times, and it is contained in the usual time-zero sigma-algebra F0. The Brownian germ sigma-algebra at zero Natural and usual augmented Brownian filtrations

[F2]

For every bounded Borel functional Φ of the future path and every s≥0, E[Φ((Bs+t)t≥0)∣Fs]=ΨΦ(Bs) almost surely, where ΨΦ(x)=∫Φ(x+w)μ(dw), and likewise with the raw past in place of Fs. Future-path Markov property

[F3]

Conditional-expectation versions are characterized by their event integrals, and B0=0 almost surely. Conditional expectation as an ae class Conditional expectation is unique almost surely Brownian motion

[F4]

AC supplies the conditional-expectation interface of [F3]. The Axiom of Choice

Proof

technique · direct
1.1F1given

Since A∈F0+0=⋂t>0Ft0, one has A∈Ft0 for every t>0, hence A∈σ(⋃t>0Ft0)=F∞0=σ(Bt:t≥0); equivalently A={B∈A0} for the corresponding product-measurable set A0 of the path space, that is, A is an event of the sigma-algebra generated by the whole future path (Bt)t≥0. By [F1] we also have A∈F0.

1.2F2F3given

Fix any F0-event A′ and any product-measurable path set Γ⊆R[0,∞). Let j:C([0,∞),R)→R[0,∞) be the measurable inclusion from [F2]. By [F2] at s=0 for the bounded Borel functional 1Γ of the future path, E[1Γ((Bt)t≥0)∣F0]=Ψ1Γ(B0) almost surely; because B0=0 almost surely and μ is Wiener measure on the continuous path space, Ψ1Γ(0)=∫C1Γ(j(w))μ(dw)=μ(j−1(Γ)). Thus the conditional expectation is the constant μ(j−1(Γ)). The event-integral characterization in [F3] therefore gives P(A′∩{(Bt)t≥0∈Γ})=P(A′)μ(j−1(Γ)); in particular, the product-space future path is independent of the completed time-zero sigma-algebra.

2.1step 1.1step 1.2

Apply step 1.2 to A′=A and to the path set Γ:=A0 supplied by step 1.1, so that {(Bt)t≥0∈Γ}=A. Taking A′=Ω in step 1.2 also gives P(A)=μ(j−1(Γ)). Hence P(A)=P(A∩A)=P(A)μ(j−1(Γ))=P(A)2, so P(A)∈{0,1}.

3.1F3F4step 2.1∎

Step 2.1 classifies the number P(A), not the set A. For example, a Brownian realization may contain a null exceptional outcome at which B0≠0; then {B0≠0}∈F00⊆F0+0 can be nonempty and proper while having probability zero. No right-continuity of the raw filtration at zero is used, only the containment of the germ in the usual time-zero sigma-algebra and the future-path independence at s=0. AC is used only through [F4] in the conditional-expectation characterization of step 1.2.

Source notes

Durrett, Theorem 7.2.3, and Sousi, Theorem 6.13, prove the zero-one law from the independence of the future increments from the germ. The proof above consumes the future-path theorem at s=0 in the completed filtration, so completion causes no gap, and it avoids the reverse-martingale formulation.

Depends on

Used by

Dependency tree · two levels

36 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