Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)
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.

Doob decomposition of an integrable adapted process

Statement

Assume AC. Every integrable adapted real X has a unique Doob decomposition up to almost-sure equality at each time. It is given by A0=0 and An=k=1nE[XkXk1Fk1],Mn=XnAn. Two decompositions agree outside a single measurable null set at all times. The normalization is that of Compensator and doob decomposition.

Facts & Assumptions

Given: The hypotheses and conventions in the statement.

[F1]

Under AC every integrable input has a measurable integrable conditional version. Conditional expectation as an ae class.

[F2]

Finite linear combinations remain integrable and their integrals are linear. The Lebesgue integral is linear on L1(μ).

[F4]

Conditional expectation is linear, order preserving and expectation preserving. Basic algebra and order properties of conditional expectation.

[F5]

An integrable variable measurable for the conditioning sigma-algebra conditions to itself. Conditioning a known variable and an independent variable.

[F6]

Martingales have conditionally centered increments, and sums of such increments with an integrable known initial value are martingales. Martingales and martingale differences correspond.

[F7]

Countable measurable null unions are null. Finite and countable subadditivity of measures.

[F8]

AC supplies the inherited conditional-expectation existence and any stated choice of versions. The Axiom of Choice.

Proof

technique · direct
1.1

First repair the integral foundation inherited by RN and conditional expectation. Augment any finite disjoint display of a nonnegative simple function by the complement with coefficient 0. Intersections of two augmented displays partition the whole space and have equal coefficients wherever nonempty, so finite additivity and 0(+)=0 prove representation independence. Common refinements give simple monotonicity and additivity; handle scalar 0 directly and positive scalars termwise. Supremum over simple minorants and the sets {fjcs}, 0<c<1, give monotone convergence; increasing simple approximations then give nonnegative additivity. Positive/negative and real/imaginary decompositions give finite L1 linearity. With these facts substituted at the affected foundation, the cited RN proof gives its density, and its event-integral existence and uniqueness argument gives the conditional-expectation class and algebra in [F1], [F4] and [F5]. Each Vk=XkXk1 is therefore real measurable and integrable, since EVkEXk+EXk1. AC permits choosing a finite real integrable Fk1-measurable version ak of its conditional expectation for every k1. Set A0=0, An=k=1nak, and Mn=XnAn. For kn one has Fk1Fn1; therefore An is predictable for n1. Finite sums and differences show that A is integrable and M is adapted and integrable.

givenF1F2F3F8construct
2.1

The increment MnMn1=Vnan has conditional expectation anan=0 given Fn1, by linearity and known-variable conditioning. Since M0=X0 is integrable and F0-measurable, [F6] makes M a martingale. The displayed decomposition holds pointwise for the chosen representatives.

F4F5F6step 1.1
3.1

If X=M~+A~ is another normalized decomposition, then A~nA~n1 is integrable and Fn1-measurable: for n=1 use A~0=0, and for n>1 use predictability and nesting. Conditioning the decomposition increment and using the zero martingale drift gives E[VnFn1]=A~nA~n1 a.s. Thus these increments equal an a.s. Induction from zero gives A~n=An and then M~n=Mn a.s. for each n. The sets where either equality fails are ambient measurable null sets; their countable union is null by [F7]. Off that one set both entire sequences agree. No completeness of the filtration is used.

givenF4F5F6F7step 1.1step 2.1

Depends on

Used by

Dependency tree · two levels

33 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