Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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.

Continuous-time filtrations and all-pairs martingales

Definition

Assume the Axiom of Choice. On a probability space (Ω,F,P), a continuous-time filtration is a family (Ft)t0 of sub-sigma-algebras of F such that FsFt whenever 0st. A process X=(Xt)t0 is adapted when Xt is measurable from (Ω,Ft) to its state space at every t.

For any process of random elements X=(Xt)t0, its natural filtration is

FtX=σ ⁣({Xu1(C):0ut, C measurable in the state space of Xu}).

The generated sigma-algebra exists by Nonempty intersections of sigma-algebras are sigma-algebras, so the generated sigma-algebra exists and is minimal. Its generator families are nested in t, so (FtX)t0 is a filtration; every Xt is FtX-measurable, and minimality makes this the smallest filtration to which X is adapted. No completion or right-continuous augmentation is included.

A real process M=(Mt)t0 is an all-pairs continuous-time martingale relative to (Ft) when:

  1. M is adapted;
  2. EMt< for every t0; and
  3. for every 0st, E[MtFs]=Msalmost surely.

The equality in clause 3 is equality of the almost-everywhere classes in Conditional expectation as an ae class. At s=t it is the known-variable identity. The word “continuous-time” specifies the index set; it does not assert path continuity. Likewise the definition imposes neither right continuity nor completeness on the filtration. AC is declared exactly because the library's conditional-expectation existence theorem uses it; the filtration, adaptation, and natural-filtration constructions make no choices.

Source notes

Sousi, Section 2 and Definition 2.1, printed pp. 13--14, gives natural filtrations, adaptation, integrability, and the all-pairs martingale identity in discrete time. Section 3.1, printed pp. 28 and 33, replaces the index set by R+, defines continuous-time filtrations and adaptation, and states that the martingale definition is unchanged. The nonaugmentation and almost-everywhere-class conventions are made explicit here to match the library's conditional-expectation interface.

Depends on

Used by

Dependency tree · two levels

16 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