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.

Ito isometry for elementary integrands

Statement

Assume the Axiom of Choice and the standing hypothesis (H) of Elementary predictable Brownian integrands. Let H be an elementary predictable integrand on [0,T] with representation Hs=k=0m1ξk1(tk,tk+1](s) and defining sums It(H) Ito integral of an elementary predictable process. Extend those sums to [0,) by setting It(H):=IT(H) for tT. Then tIt(H) is a continuous square-integrable martingale relative to (Ft) Continuous-time adapted processes and martingales, and for every t[0,T] E[It(H)2]=E0tHs2ds=k=0m1E[ξk2](ttk+1ttk). By the representation independence of Elementary Ito integrals do not depend on step representation both sides depend only on the (dtP)-class of H.

Facts & Assumptions

Given: AC, the standing hypothesis (H), a horizon T>0, an elementary representation Hs=k=0m1ξk1(tk,tk+1](s) with bounded Ftk-measurable ξk, its defining sums It(H), and 0stT.

[F1]

For 0u<v, the increment BvBu is independent of Fu and has law N(0,vu), hence mean 0 and second moment vu; for bounded Fu-measurable Z, E[Z(BvBu)Fu]=0 and E[Z(BvBu)2Fu]=Z(vu) almost surely. Elementary predictable Brownian integrands Brownian covariance is equivalent to independent stationary normal increments Gaussian even moments for Brownian increments Taking out what is known

[F2]

If YL1(P) is independent of a sub-sigma-algebra G then E[YG]=EY almost surely; here Y=BvBu and G=Fu qualify by [F1]. Independent sigma-algebras and independent events Expectations factor over finite products of independent random variables Conditional expectation is unique almost surely

[F3]

I(H) is adapted, I0(H)=0, and each It(H) is a finite sum of products of bounded coefficients with Gaussian increments, so EIt(H)< and EIt(H)2<; path continuity holds on the Brownian continuity event. Ito integral of an elementary predictable process

[F4]

For HG and integrable Z, E[E[ZG]H]=E[ZH], and E[ZWG]=ZE[WG] whenever WL1(P), Z is finite real and G-measurable, and both ZW and ZE[WG] are integrable. Tower property of conditional expectation Taking out what is known

[F5]

A martingale is exactly an adapted process with EMt< and E[MtFr]=Mr almost surely for all rt. Continuous-time adapted processes and martingales

[F6]

AC is declared for the conditional-expectation interface. The Axiom of Choice

Proof

technique · direct
1.1

Refining the partition of H if necessary so that s is a partition point, write the increments of the defining sum between the deterministic times st as It(H)Is(H)=kξk(Btuk+1Btuk)kξk(Bsuk+1Bsuk) over the refined partition 0=u0<<un=T; this is a finite rearrangement and does not change the values by the definition of the sums. Term by term, a block with uk+1s contributes 0, a block with ukt contributes 0, and every remaining block contributes ξk(BakBbk) with bk=max(s,uk) and ak=tuk+1, so that sbkakT and ξk is Fuk-measurable with FukFbk.

F3given
1.2

For each such block, BakBbk is independent of Fbk with mean 0 and second moment akbk by (H): E[BakBbkFbk]=0 and E[(BakBbk)2Fbk]=akbk almost surely.

F1F2given
2.1

For every remaining block, E[ξk(BakBbk)Fs]=E[ξkE[BakBbkFbk]Fs]=0 almost surely, because FsFbk, ξk is bounded and Fbk-measurable, and the inner conditional expectation vanishes by step 1.2; summing the finitely many blocks gives E[It(H)Is(H)Fs]=0, so E[It(H)Fs]=Is(H) almost surely by linearity of conditional expectation and the Fs-measurability of Is(H).

F4step 1.1step 1.2
2.2

For the variance, write Δkt:=Bttk+1Bttk for the blocks of the original partition, so that It(H)=kξkΔkt. For k<l the random variable Δkt is Ftl-measurable, because ttk+1tk+1tl, and ξk,ξlFtl; Each increment is in L2, and 2aba2+b2 shows that a product of two increments is integrable; bounded coefficients preserve these bounds. In the off-diagonal use of [F4], take W=Δlt and Z=ξkΔktξl; WL1, ZWL1, and ZE[WFtl]=0 is integrable. In the diagonal use, W=(Δkt)2L1 and Z=ξk2 is bounded. By (H) applied to the increment over the interval (tl,ttl+1] (which is empty, hence contributes 0, when ttl), E[ΔltFtl]=0 almost surely, so the tower property and taking out what is known give E[ξkΔktξlΔlt]=E[ξkΔktξlE[ΔltFtl]]=0. For the diagonal terms, the same identity gives E[ξk2(Δkt)2]=E[ξk2E[(Δkt)2Ftk]]=E[ξk2](ttk+1ttk), where the block contributes 0 when ttk.

F1F4step 1.2
3.1

Summing the diagonal terms of step 2.2 and using Hs2=kξk21(tk,tk+1](s) gives EIt(H)2=k=0m1E[ξk2](ttk+1ttk)=E0tHs2ds, finite because there are finitely many bounded coefficients.

step 2.2F3
4.1

Steps 2.1, 3.1 and [F3] show the martingale and isometry assertions on [0,T]. The constant extension from the statement is adapted and continuous; if s<T<t, the already proved identity gives E[It(H)Fs]=E[IT(H)Fs]=Is(H), while for Tst both sides equal IT(H). Thus [F5] makes the extended process a continuous square-integrable martingale on [0,). Independence of the representation is the content of item 6. AC is used only through the conditional-expectation facts [F2], [F4] and the Brownian interface (H); the partition, the blocks and the sums are fixed by the representation.

step 2.1step 3.1F3F5F6given

Source notes

Lawler, Proposition 3.2.1, proves precisely this package for simple processes: the integral is a martingale, and its variance is the integral of the square of the integrand (Proposition 3.2.1(iii)). The proof here separates the conditional-centering identity from the variance expansion; both use only independence and mean zero of future increments, not their full Gaussian law beyond the second moment.

Depends on

Used by

Dependency tree · two levels

63 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