Alphabeta Math
CorollaryStatement: 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.

Square-integrable Brownian terminal variables have Ito representations

Statement

Assume the Axiom of Choice. Let B be a standard Brownian motion with usual augmented natural filtration (Ft) Natural and usual augmented Brownian filtrations, fix T>0, and let XL2(FT). Then there is a predictable process H on [0,T] with E0THs2ds< such that X=EX+0THsdBsalmost surely, and H is unique up to (dtP)-null sets. Moreover the conditional-expectation martingale tE[XFt] agrees, up to indistinguishability on [0,T], with the continuous process EX+0tHsdBs.

Facts & Assumptions

Given: AC, a standard Brownian motion B with usual augmented filtration (Ft), a horizon T>0, and XL2(FT).

[F1]

Representation theorem, L2 clause. For every ZL2(FT) there is a predictable H with finite energy on [0,T] such that Z=EZ+0THdB almost surely; the conditional-expectation martingale E[ZFt] agrees up to indistinguishability with EZ+0tHdB, and H is unique modulo (dtP)-null sets. Brownian-filtration martingale representation

[F2]

Isometry and martingale property. For finite-energy predictable H the integral 0THdB has mean zero and L2 norm squared E0TH2ds, and the process t0tHdB has a continuous version that is a martingale; if two finite-energy integrands have integrals with the same terminal value almost surely, their difference has zero L2(dtP) norm. Ito isometry and linearity in predictable L2 The Ito integral process has a continuous martingale version Ito integral for square-integrable predictable processes Locally square-integrable predictable Brownian integrands

[F3]

Conditional expectation. E[XFt] is the unique a.s. class with AE[XFt]dP=AXdP for all AFt, and the tower property identifies E[XFT]=X as an a.s. class. Conditional expectation as an ae class Tower property of conditional expectation Continuous-time adapted processes and martingales

[F4]

AC bookkeeping. Choice is an ambient assumption, not a source of Brownian or conditional-expectation data. It is declared because the representation theorem [F1], the Ito construction and martingale interfaces [F2], and the conditional-expectation interfaces [F3] are themselves stated under AC. The Axiom of Choice

Proof

technique · direct
1.1

Existence: [F1] applied to the given XL2(FT) supplies a predictable finite-energy H with X=EX+0THdB almost surely, and the same clause identifies the conditional-expectation martingale with the continuous integral process up to indistinguishability.

F1
2.1

Uniqueness: if H and K both represent XEX, then 0T(HK)dB=0 almost surely, so by the isometry of [F2] E0T(HK)2ds=0, which is exactly H=K (dtP)-almost everywhere.

F2step 1.1
3.1

Endpoint and degenerate cases: for X constant, H=0 and the representation reads X=EX; for X=E[XFT] the tower property [F3] supplies the conditional-expectation interpretation used in the last sentence of the statement; the uniqueness is modulo (dtP)-null sets, so two integrands differing on a dt-null set of times or on a P-null set of paths are the same element of L2(dtP); and AC is inherited through each of [F1]--[F3], as recorded in [F4].

F1F2F3F4step 2.1

Source notes

Van der Vaart, Theorem 6.6, obtains this L2 terminal form as the first stage of the martingale representation theorem; here the corollary is read off directly from that clause, with uniqueness supplied by the Ito isometry.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

75 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