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.

The Ito integral process has a continuous martingale version

Statement

Assume the Axiom of Choice and the standing hypothesis (H) of Elementary predictable Brownian integrands. Let H be a predictable process with E0THs2ds< for every finite T. Then there is an adapted process M=(Mt)t0 with continuous paths such that Mt=0tHsdBs almost surely for every t0 Ito integral for square-integrable predictable processes, and M is a square-integrable martingale relative to (Ft) Continuous-time adapted processes and martingales: EMt2=E0tHs2ds< for every t. Any two such continuous versions agree at every time on one measurable event of probability one; in particular the continuous version is unique in this common-full-measure-event sense, and it is the only continuous square-integrable martingale whose value at each deterministic t is the integral class.

This conclusion is deliberately distinguished from the exact definition of indistinguishability in Process law, modification, and indistinguishability. On a noncomplete probability space the full equality set, although it contains the measurable probability-one event constructed below, need not itself be measurable. On a complete probability space the two notions coincide, because the complement of the equality set is then a measurable subset of a null set.

Facts & Assumptions

Given: AC, the standing hypothesis (H), a finite-energy predictable H with E0TH2ds< for all finite T, and a horizon T>0.

[F1]

For every δ>0 there is a bounded elementary predictable G with HGL2(dtP)<δ. Density asserts existence, not an enumeration of all elementary integrands. Density of elementary predictable processes in predictable L2

[F2]

For elementary J the process I(J) is a continuous square-integrable martingale with E(It(J)Is(J))2=EstJ2du for st, and EIT(J)2=E0TJ2du. Ito integral of an elementary predictable process Ito isometry for elementary integrands

[F3]

Doob's L2 maximal inequality: for a discrete martingale Y0,,YN with YNL2, EmaxkNYk24EYN2; the sampled family (IkT/2m(J))k is a discrete martingale for the filtration (FkT/2m)k, by the tower property. Doob Lp maximal inequality Tower property of conditional expectation

[F4]

If a sequence 0ZnZ of nonnegative random variables increases pointwise, then EZnEZ; the dyadic grids Dm:={kT/2m:0k2m} are nested with union a countable dense subset D of [0,T], so supqDIq(J)=limmmaxqDmIq(J). Monotone convergence for the integral

[F5]

The rationals are dense in R, and each rational is a limit of dyadic rationals k/2n; a continuous function on [0,T] therefore satisfies supt[0,T]f(t)=supqDf(q). The rationals embed densely in the reals

[F6]

For every t the class 0tHdB is the L2(P)-limit of It(Hn) for every admissible elementary sequence HnH, and 0tHdB22=E0tH2ds; the integration map is linear and isometric in the predictable L2 variable. Ito integral for square-integrable predictable processes The general Ito integral is well defined Ito isometry and linearity in predictable L2

[F7]

If XnX in L2(P) then EXnXXnX20, and conditional expectations are L1-contractive: E[XnG]E[XG]1EXnX. Cauchy-Schwarz for random variables Basic algebra and order properties of conditional expectation

[F8]

AC supplies a selection from each nonempty set of elementary representations satisfying a prescribed error tolerance, simultaneously over countably many tolerances and integer horizons. The Axiom of Choice AC supplies countable selections and prescribed serial paths

Proof

technique · direct
1.1

Fix T>0 and choose, using [F8] on the nonempty sets supplied by [F1] with tolerance 22n, bounded elementary predictable Hn with HnHL2(dtP)22n; write Xtn:=It(Hn) for the continuous elementary process of [F2].

F1F2F8given
1.2

For every elementary predictable J and every S>0, writing the path supremum as its measurable version on the scaled dyadic grid, EsuptSIt(J)24E0SJ2du: on the full-measure event where I(J) is continuous, [F5] identifies the supremum over [0,S] with the supremum over the scaled dyadic grid, [F4] writes the latter as the increasing limit of the finite maxima over the nested grids Dm, [F3] bounds EmaxqDmIq(J)24EIS(J)2=4E0SJ2du for every m, and monotone convergence passes the bound to the limit.

F2F3F4F5
2.1

For each n, Hn+1Hn is elementary on a common refinement and Hn+1HnL2(dtP)22(n+1)+22n212n; applying step 1.2 to J=Hn+1Hn gives Ean24(212n)2=244n for the measurable random variable an:=suptDXtn+1Xtn, which equals the full supremum on the common event of continuity.

F2step 1.1step 1.2
3.1

Consequently En12nan2=n12nEan2n1243n< by monotone convergence for the nonnegative series [F4], so n2nan2< almost surely; the Cauchy--Schwarz inequality nan=n(2n/2an)2n/2(n2nan2)1/2(n2n)1/2 then gives nan< almost surely, on a measurable event AT of probability one, intersected with the common continuity event of the elementary processes.

F4step 2.1
4.1

On AT the sequence Xn converges uniformly on [0,T] to a limit; put Lt:=lim supnXtn and define Mt(T):=Lt when Lt is finite, and Mt(T):=0 otherwise. This is real-valued and Ft-measurable: Lt is an extended-real measurable limit superior and its finite-value event belongs to Ft. The resulting variable satisfies Mt(T)=limnXtn almost surely for every t; on AT the paths of M(T) are continuous, being uniform limits of continuous paths.

F2step 3.1
5.1

For every t[0,T] the sequence Xtn=It(Hn) converges to 0tHdB in L2(P) by [F6] applied to the truncations Hn1[0,t]H1[0,t]; combined with step 4.1 and the almost-sure uniqueness of limits, Mt(T)=0tHdB almost surely for every t[0,T].

F6step 4.1
5.2

For every t[0,T], E(Mt(T))2=limnE(Xtn)2=limnE0t(Hn)2ds=E0tH2ds<, using [F6] and the L2-norm continuity of the elementary integrals; hence M(T) is square-integrable.

F6step 2.1step 4.1
6.1

For 0stT and n, E[XtnFs]=Xsn by [F2], and step 5.1 and [F7] give XtnMt(T) and XsnMs(T) in L1(P) as well, so [F7] lets the conditional expectations pass to the limit: E[Mt(T)Fs]=Ms(T) almost surely.

F2F7step 5.1
7.1

Steps 4.1, 5.1, 6.1 and 5.2 show that M(T) is an adapted continuous square-integrable martingale version on [0,T]. If N is another continuous version on [0,T], then Mq(T)=Nq almost surely for each rational q[0,T]; intersecting the countably many measurable full-measure events and the two continuity events, and then invoking continuity, gives Mt(T)=Nt for every t[0,T] on one measurable event of probability one.

F5step 4.1step 5.1step 6.1step 5.2
8.1

Apply the construction on the horizons T=m, m=1,2,; two versions on adjacent horizons agree on the smaller one by the uniqueness of step 7.1 applied there, since the restriction of the larger-horizon version is a continuous version on the smaller horizon. For t0 put m(t):=max(1,t) and define Mt:=Mt(m(t)). This is well typed and Ft-measurable. On the intersection of the countably many overlap-agreement and continuity events, it coincides at every time with the compatible local versions, so its path is continuous. At each deterministic time it is a version of 0tHdB; hence the local martingale identities show that M is a square-integrable martingale with EMt2=E0tH2ds. Uniqueness on one measurable full-measure event over [0,) follows from the same rationals-and-continuity argument. AC supplies the approximants of step 1.1 simultaneously for all integer horizons, and is also inherited through the declared ambient interfaces.

step 7.1F8given

Source notes

Van der Vaart, Theorem 5.26(i)--(iii), proves the martingale and continuity conclusions using maximal estimates and an almost-sure uniformly convergent subsequence. Lawler, Proposition 3.2.4, gives a related summable-error uniform-convergence criterion for the integrands treated there. The proof here follows the summable-error route, which is why no almost-sure-subsequence theorem is needed: the weighted series n2nan2 is summable in expectation, and Cauchy--Schwarz converts it into almost-sure summability of the sup norms.

Depends on

Used by

Dependency tree · two levels

72 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