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 be an elementary predictable integrand on with representation and defining sums Ito integral of an elementary predictable process. Extend those sums to by setting for . Then is a continuous square-integrable martingale relative to Continuous-time adapted processes and martingales, and for every By the representation independence of Elementary Ito integrals do not depend on step representation both sides depend only on the -class of .
Facts & Assumptions
Given: AC, the standing hypothesis (H), a horizon , an elementary representation with bounded -measurable , its defining sums , and .
For , the increment is independent of and has law , hence mean and second moment ; for bounded -measurable , and 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
If is independent of a sub-sigma-algebra then almost surely; here and qualify by [F1]. Independent sigma-algebras and independent events Expectations factor over finite products of independent random variables Conditional expectation is unique almost surely
is adapted, , and each is a finite sum of products of bounded coefficients with Gaussian increments, so and ; path continuity holds on the Brownian continuity event. Ito integral of an elementary predictable process
For and integrable , , and whenever , is finite real and -measurable, and both and are integrable. Tower property of conditional expectation Taking out what is known
A martingale is exactly an adapted process with and almost surely for all . Continuous-time adapted processes and martingales
AC is declared for the conditional-expectation interface. The Axiom of Choice
Proof
Refining the partition of if necessary so that is a partition point, write the increments of the defining sum between the deterministic times as over the refined partition ; this is a finite rearrangement and does not change the values by the definition of the sums. Term by term, a block with contributes , a block with contributes , and every remaining block contributes with and , so that and is -measurable with .
For each such block, is independent of with mean and second moment by (H): and almost surely.
For every remaining block, almost surely, because , is bounded and -measurable, and the inner conditional expectation vanishes by step 1.2; summing the finitely many blocks gives , so almost surely by linearity of conditional expectation and the -measurability of .
For the variance, write for the blocks of the original partition, so that . For the random variable is -measurable, because , and ; Each increment is in , and shows that a product of two increments is integrable; bounded coefficients preserve these bounds. In the off-diagonal use of [F4], take and ; , , and is integrable. In the diagonal use, and is bounded. By (H) applied to the increment over the interval (which is empty, hence contributes , when ), almost surely, so the tower property and taking out what is known give . For the diagonal terms, the same identity gives , where the block contributes when .
Summing the diagonal terms of step 2.2 and using gives , finite because there are finitely many bounded coefficients.
Steps 2.1, 3.1 and [F3] show the martingale and isometry assertions on . The constant extension from the statement is adapted and continuous; if , the already proved identity gives , while for both sides equal . Thus [F5] makes the extended process a continuous square-integrable martingale on . 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.
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
- Ito integral of an elementary predictable process
- Elementary predictable Brownian integrands
- Elementary Ito integrals do not depend on step representation
- Continuous-time adapted processes and martingales
- Conditional expectation as an ae class
- Conditional expectation is unique almost surely
- Taking out what is known
- Tower property of conditional expectation
- Expectations factor over finite products of independent random variables
- Independent sigma-algebras and independent events
- Brownian covariance is equivalent to independent stationary normal increments
- Gaussian even moments for Brownian increments
- The Axiom of Choice
- AC supplies countable selections and prescribed serial paths
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
- Gregory F. Lawler, Stochastic Calculus: An Introduction with Applications, Proposition 3.2.1 (standard reference, not scraped)