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 and linearity in predictable L2

Statement

Assume the Axiom of Choice and the standing hypothesis (H) of Elementary predictable Brownian integrands. Fix $T > 0$ . For predictable $H, K$ with finite energy $E \int_{0}^{T} H^{2} d s, E \int_{0}^{T} K^{2} d s < \infty$ the integrals $\int_{0}^{T} H d B$ of Ito integral for square-integrable predictable processes satisfy $\int_{0}^{T} (H + K) d B = \int_{0}^{T} H d B + \int_{0}^{T} K d B, \int_{0}^{T} (a H) d B = a \int_{0}^{T} H d B (a \in R),$ and the identities are equalities of $L^{2} (P)$ -classes (almost sure equalities). Moreover the map $H \mapsto \int_{0}^{T} H d B$ is an isometry, $E (\int_{0}^{T} H d B)^{2} = E \int_{0}^{T} H^{2} d s = ∥ H ∥_{L^{2} (d t \otimes P)}^{2},$ it takes values in the mean-zero subspace of $L^{2} (P)$ , and the bilinear cross identity $E [(\int_{0}^{T} H d B) (\int_{0}^{T} K d B)] = E \int_{0}^{T} H_{s} K_{s} d s$ holds for all such $H, K$ . In particular the image of the map is a closed subspace of $L^{2} (P)$ isometric to the predictable $L^{2}$ space of $H$ 's, and $H \mapsto \int_{0}^{T} H d B$ is injective up to the $(d t \otimes P)$ -class.

Facts & Assumptions

Given: AC, the standing hypothesis (H), $T > 0$ , finite-energy predictable $H, K$ , elementary sequences $H^{n} \to H$ and $K^{n} \to K$ in $L^{2} (d t \otimes P)$ , and $a \in R$ .

[F1]

$∥ H^{n} + K^{n} - (H + K) ∥_{2} \leq ∥ H^{n} - H ∥_{2} + ∥ K^{n} - K ∥_{2} \to 0$ and $∥ a H^{n} - a H ∥_{2} = ∣ a ∣ ∥ H^{n} - H ∥_{2} \to 0$ , so $H^{n} + K^{n}$ and $a H^{n}$ are admissible approximating sequences for $H + K$ and $a H$ . The $L^{p}$ norm descends to the quotient and makes $L^{p}$ a normed space for $1 \leq p \leq \infty$

[F2]

For elementary $G$ one has $I_{T} (G) =$ the elementary sum, $E I_{T} (G)^{2} = E \int_{0}^{T} G^{2}$ , $E I_{T} (G) = 0$ , and for elementary $G, G^{'}$ on a common refinement $E [I_{T} (G) I_{T} (G^{'})] = E \int_{0}^{T} G G^{'}$ . Ito integral of an elementary predictable process Ito isometry for elementary integrands Cross Ito isometry Continuous-time adapted processes and martingales

[F3]

Each integral $\int_{0}^{T} G d B$ is the $L^{2} (P)$ -limit of $I_{T} (G^{n})$ for any admissible elementary sequence, and the limit is independent of the sequence. Ito integral for square-integrable predictable processes The general Ito integral is well defined

[F4]

On the quotient space $L^{2} (P)$ , $L^{2}$ -convergence implies convergence of norms and of expectations: $∣ ∥ X_{n} ∥_{2} - ∥ X ∥_{2} ∣ \leq ∥ X_{n} - X ∥_{2}$ and $∣ E X_{n} - E X ∣ \leq ∥ X_{n} - X ∥_{2}$ ; and the predictable $L^{2}$ space, like every $L^{2}$ space, is complete. The $L^{p}$ norm descends to the quotient and makes $L^{p}$ a normed space for $1 \leq p \leq \infty$ Basic algebra and order properties of conditional expectation Riesz-Fischer completeness of $L^{p}$ for $1 \leq p \leq \infty$

[F5]

The algebraic identities $(X + Y)^{2} - (X - Y)^{2} = 4 X Y$ and $X^{2} - Y^{2} = (X - Y) (X + Y)$ hold for real random variables, and $L^{2} (P)$ is a real vector space of classes. Conditional expectation as an ae class

[F6]

AC is declared for the ambient interfaces. The Axiom of Choice

Proof

technique · direct

1.1

For each $n$ the elementary integrals are linear on a common refinement, $I_{T} (H^{n} + K^{n}) = I_{T} (H^{n}) + I_{T} (K^{n})$ and $I_{T} (a H^{n}) = a I_{T} (H^{n})$ identically; by [F2] the isometry $E I_{T} (G)^{2} = E \int_{0}^{T} G^{2}$ , the mean identity $E I_{T} (G) = 0$ for elementary $G$ , and the cross identity hold at every index.

F2given

1.2

By [F1] the sequences $H^{n} + K^{n}$ and $a H^{n}$ are admissible for $H + K$ and $a H$ , so [F3] gives $I_{T} (H^{n} + K^{n}) \to \int_{0}^{T} (H + K) d B$ and $I_{T} (a H^{n}) \to \int_{0}^{T} (a H) d B$ in $L^{2} (P)$ , as well as $I_{T} (H^{n}) \to \int_{0}^{T} H d B$ and $I_{T} (K^{n}) \to \int_{0}^{T} K d B$ .

F1F3given

2.1

Letting $n \to \infty$ in the linear identities of step 1.1 and using uniqueness of $L^{2} (P)$ -limits, $\int_{0}^{T} (H + K) d B = \int_{0}^{T} H d B + \int_{0}^{T} K d B$ and $\int_{0}^{T} (a H) d B = a \int_{0}^{T} H d B$ almost surely.

F3step 1.1step 1.2

2.2

Taking the limit in the elementary isometry of step 1.1 gives $E (\int_{0}^{T} H d B)^{2} = \lim_{n} E I_{T} (H^{n})^{2} = \lim_{n} E \int_{0}^{T} (H^{n})^{2} = ∥ H ∥_{L^{2} (d t \otimes P)}^{2}$ by [F4] applied to the $L^{2} (P)$ -limits and to the $L^{2} (d t \otimes P)$ -convergence $H^{n} \to H$ . Likewise $E \int_{0}^{T} H d B = \lim_{n} E I_{T} (H^{n}) = 0$ , and the triangle inequality gives $∣ E \int_{0}^{T} H d B ∣ \leq ∥ \int_{0}^{T} H d B ∥_{2} < \infty$ . So the image is mean-zero and isometric.

F4step 1.1step 1.2

3.1

For the cross identity use $4 X Y = (X + Y)^{2} - (X - Y)^{2}$ with $X = \int_{0}^{T} H d B$ and $Y = \int_{0}^{T} K d B$ : by step 2.1, $4 E [X Y] = E (\int_{0}^{T} (H + K) d B)^{2} - E (\int_{0}^{T} (H - K) d B)^{2} = ∥ H + K ∥_{2}^{2} - ∥ H - K ∥_{2}^{2} = 4 E \int_{0}^{T} H K d s$ by step 2.2. All terms are finite by step 2.2.

F5step 2.1step 2.2

4.1

Steps 2.1--3.1 are exactly the linearity, isometry, mean-zero and cross-identity claims; injectivity follows because $∥ \int_{0}^{T} (H - K) d B ∥_{2} = ∥ H - K ∥_{L^{2} (d t \otimes P)}$ , and closedness of the image follows because the image of a complete space under an isometry onto it is complete, hence closed, with the target metric restricted: the domain of classes is complete by [F4], and the isometry carries its Cauchy sequences to Cauchy sequences whose limits are the images of the domain limits. AC enters only through the declared ambient interfaces [F6]; the approximating sequences are the given ones and the limits are unique.

step 2.1step 3.1F4F6given∎

Source notes

Lawler, Sections 3.2.2--3.2.3, proves linearity and the variance rule for the extended integral by approximation. The presentation here keeps the two descents separate: item 11 supplies well-definedness of the limit, and the elementary isometry and cross isometry of items 7 and 8 are passed to the limit through the continuity of the $L^{2}$ norm and of the expectation.

Depends on

Used by

Deterministic Ito integrals are Gaussian Corollary
Square-integrable Brownian terminal variables have Ito representations Corollary
The Brownian square martingale Corollary
The exponential Brownian martingale Corollary
The ordinary chain rule fails for Brownian motion Counterexample
Covariance of deterministic Ito integrals Example
Harmonic functions of planar Brownian motion Example
Integral of Brownian motion against itself Example
Ito formula for Brownian powers Example
Brownian-filtration martingale representation Theorem
Doob maximal bound for the Ito integral Theorem
Integration by parts for Brownian Ito processes Theorem
Localized Ito integral Theorem
Multidimensional Ito formula for Brownian-driven processes Theorem
One-dimensional Ito formula Theorem
Quadratic covariation of Brownian Ito processes Theorem
Quadratic variation of an Ito integral Theorem
Space-time harmonic functions yield Brownian local martingales up to exit lifetime Theorem
The Ito integral process has a continuous martingale version Theorem

Dependency tree · two levels

54 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, Sections 3.2.2-3.2.3 (standard reference, not scraped)