15 Stochastic integral
The lecture notes at this link as well as chapter 18 of [ Kal21 ] are good references for this chapter. Some of the proofs are taken from [ Pas24 ] .
15.1 Stochastic integral
TODO: relax continuity of the martingales, be clear about continuous quadratic variation vs general càdlàg quadratic variation.
For \(M\) a local martingale and \(X\) a stochastic process, we will use integrals of the form \(\int _0^t X_s \: d\langle M \rangle _s\) . Let’s explain what those integrals mean. For all \(\omega \in \Omega \), \(\langle M \rangle (\omega )\) is a right-continuous non-decreasing function (called a Stieltjes function in Mathlib) so it defines a measure on \(\mathbb {R}_+\), denoted by \(d\langle M \rangle \) . Then, for each fixed \(\omega \in \Omega \), if the function \(s \mapsto X_s(\omega )\) is integrable with respect to the measure \(d\langle M \rangle (\omega )\), the Bochner integral \(\int _0^t X_s(\omega ) \: d\langle M \rangle (\omega )\) is well-defined. By \(\int _0^t X_s \: d\langle M \rangle _s\), we mean the random variable \(\omega \mapsto \int _0^t X_s(\omega ) \: d\langle M \rangle (\omega )\) . If we also vary \(t\), we get a stochastic process.
15.1.1 Itô isometry
The predictable \(\sigma \)-algebra on \(T \times \Omega \) is a sub-\(\sigma \)-algebra of the product \(\sigma \)-algebra \(\mathcal{B}(T) \otimes \mathcal{F}\) .
Let \(\mu \) be a measure on \(T\) and \(P\) a measure on \(\Omega \). We denote by \(L^2(\mu , P)\) the space \(L^2(T \times \Omega , \mathcal{P}, \mu \times P)\), in which \(\mathcal{P}\) is the predictable \(\sigma \)-algebra, and the measure \(\mu \times P\) is the restriction of the product measure on \(\mathcal{B}(T) \otimes \mathcal{F}\) to \(\mathcal{P}\) .
TODO: the measures should be at least finite, I guess.
TODO: we will write that a stochastic process \(X : T \to \Omega \to E\) “is in \(L^2(\mu , P)\)”, but this means that the L2 equivalence class of the function \((t, \omega ) \mapsto X_t(\omega )\) is in \(L^2(\mu , P)\) . In Lean, we can use MemLp for the uncurried function.
For \(X, Y \in L^2(\mu , P)\), we have
The norm is \(\Vert X \Vert _{L^2(\mu , P)}^2 = P\left[ \int _0^{\infty } \Vert X_t \Vert ^2 \: d\mu \right]\) .
The inner product in \(L^2\) spaces is defined as the integral of the pointwise inner products.
Any simple process in \(\mathcal{E}_{T, E}\) is in \(L^2(\mu , P)\) .
(Lean remark: we mean that the uncurried version of its coercion to a function satisfies MemLp)
A simple process is bounded by definition.
Let \(V \in \mathcal{E}_{T, E}\) and \(\mu \) a measure on \(T\) . Let \(f\) be a right-continuous non-decreasing function such that for all \(s {\lt} t\), \(\mu ((s,t]) = f(t) - f(s)\) (the CDF of \(\mu \), but that’s only defined for \(\mathbb {R}\) in Lean). Then
TODO: this proof (and the result of the lemma) assumes that the intervals defining the simple process are disjoint.
Let \(V \in \mathcal{E}_{T, E}\) , with \(V_t(\omega ) = \sum _{k=1}^n \eta _k(\omega ) \mathbb {1}_{(s_k, t_k]}(t)\) .
Let \(M\) be a square integrable martingale. We define
in which \(\mathcal{P}\) is the predictable \(\sigma \)-algebra and \(d\langle M \rangle \) is the measure induced by the quadratic variation of \(M\).
For \(V \in \mathcal{E}\) and \(M \in \mathcal{M}^2\), then \(V \bullet M \in \mathcal{M}^2\) (by Lemma 13.28) and
There are two steps to the proof.
First, in order to make sense of \(\Vert V \Vert _{L^2(M)}\), we define the natural linear map from \(\mathcal{E}\) to \(L^2(M)\) via SimpleProcess.toFun. (Informally, this is identifying \(\mathcal{E}\) as a subset \(\mathcal{E} \subseteq L^2(M)\).) This induces the \(L^2(M)\)-norm on \(\mathcal{E}\), using something like NormedSpace.induced.
Next, we show that integration \(V \mapsto V \bullet M\) is an isometry from \(\mathcal{E}\) with the \(L^2(M)\)-norm, to \(\mathcal{M}^2\). The proof is TODO.
Let \(X\in L^2(M)\) such that \(\int _0^t X_s \: d\langle M \rangle _s = 0\) for all \(t \ge 0\) a.s.. Then \(X = 0\) \((\mathbb {P} \times d\langle M \rangle )\)-almost everywhere.
For \(B\) a measurable set of \(\mathbb {R}_+\) and \(\omega \in \Omega \), let \(\nu _\omega (B) = \int _B X_s(\omega ) \: d\langle M \rangle _s(\omega )\) . This is a signed measure on \(\mathbb {R}_+\) . Then if for all \(t\), \(\int _0^t X_s(\omega ) \: d\langle M \rangle _s(\omega ) = 0\) then \(\nu _\omega ([0,t]) = 0\) for all \(t\). Those intervals generate the Borel \(\sigma \)-algebra on \(\mathbb {R}_+\), so \(\nu _\omega \) is the zero measure. Thus, for almost all \(\omega \), \(\nu _\omega \) is the zero measure.
The measure \(\nu _\omega \) is absolutely continuous with respect to the measure \(d\langle M \rangle (\omega )\) , and its Radon-Nikodym derivative is \(X(\omega )\) . Since \(\nu _\omega \) is the zero measure for almost all \(\omega \), we have that \(X(\omega ) = 0\) \(d\langle M \rangle (\omega )\)-almost everywhere for almost all \(\omega \) . Equivalently, \(X = 0\) \((\mathbb {P} \times d\langle M \rangle )\)-almost everywhere.
Let \(X, Y \in L^2(M)\) such that \(\int _0^t X_s \: d\langle M \rangle _s = \int _0^t Y_s \: d\langle M \rangle _s\) for all \(t \ge 0\) a.s.. Then \(X = Y\) almost everywhere.
By linearity of the integral, we have \(\int _0^t (X_s - Y_s) \: d\langle M \rangle _s = 0\) for all \(t \ge 0\) a.s.. Then apply Lemma 15.8 to \(X - Y\) .
Let \(X \in L^2(M)\) such that \(\langle X, V\rangle = 0\) for any simple process \(V\). Let \(A_t = \int _0^t X_s \: d\langle M \rangle _s\). Then \(A_t\) is a martingale.
By Lemma 10.41, it is enough to show that for any bounded real simple process \(V\), \(\mathbb {E}[(V \bullet A)_\infty ] = 0\) .
Let \(X \in L^2(M)\) such that \(\langle X, V\rangle = 0\) for any simple process \(V\). Then for all \(t\), \(\int _0^t X_s \: d\langle M \rangle _s = 0\).
The set of simple processes is dense in \(L^2(M)\).
Since \(L^2(M)\) is a Hilbert space, it is enough to show that if \(X \in L^2(M)\) is orthogonal to all simple processes, then \(X = 0\) . Let \(X \in L^2(M)\) such that for any simple process \(V\), \(\mathbb {E}\left[ \int _0^{\infty } X_t V_t \: d\langle M \rangle _t \right] = 0\) . Let \(A_t = \int _0^t X_s \: d\langle M \rangle _s\). It suffices to show that \(A = 0\) by Lemma 15.8 . This is proved in Lemma 15.11 .
In Lean, this is stated as: the natural linear map toFun from \(\mathcal{E}\) to \(L^2(M)\) is IsDenseInducing. The Itô isometry is then defined using IsDenseInducing.extend.
Let \(M \in \mathcal{M}^2\). Then the elementary stochastic integral map \(\mathcal{E} \to \mathcal{M}^2\) defined by \(V \mapsto V \bullet M\) extends to an isometry \(L^2(M) \to \mathcal{M}^2\).
\(\langle X \cdot M, Y \cdot M \rangle _{\mathcal{M}^2} = (XY) \cdot \langle M, N \rangle _{\mathcal{M}^2}\).
15.1.2 Local martingales
Let \(M\) be a continuous local martingale. We define \(L^2_{loc}(M)\) as the space of predictable processes \(X\) such that for all \(t \ge 0\), \(\mathbb {E}\left[ \int _0^t X_s^2 \: d\langle M \rangle _s \right] {\lt} \infty \).
Let \(M\) be a continuous local martingale and let \(X \in L^2_{loc}(M)\). We define the local stochastic integral \(X \cdot M\) as the unique continuous local martingale with \((X \cdot M)_0 = 0\) such that for any continuous local martingale \(N\), almost surely,
15.1.3 Semi-martingales
For a continuous semi-martingale \(X = M + A\) and \(V \in L^2_{semi}(X)\) (to be defined) we define the stochastic integral as
in which \(V \cdot M\) is the local stochastic integral defined in 15.16 and \(V \cdot A\) is the Lebesgue-Stieltjes integral with respect to the locally finite variation process \(A\).
For \(X = M + A\) and \(Y = N + B\), we define the covariation as
15.2 Itô formula
Let \(X\) and \(Y\) be two continuous semi-martingales. Then we have almost surely
Let \(X^1, \ldots , X^d\) be continuous semi-martingales and let \(f : \mathbb {R}^d \to \mathbb {R}\) be a twice continuously differentiable function. Then, writing \(X = (X^1, \ldots , X^d)\), the process \(f(X)\) is a semi-martingale and we have